[orbitingflea]

Part of #1634.

Summary

Formalizes an open-addressed linear-probing dictionary (Cslib.Algorithms.WordRAM.Dictionary.LinearProbing) for Dictionary.spec U V n_max (universe U, value bound V, capacity n_max) on the randomized Word RAM (SubroutineDS), reusing Hashing.KWise (isKWiseIndependentHash_trinomialPolyHash, $k = 5$).

Adapts Pagh, Pagh, and Ružić, Linear Probing with Constant Independence, SIAM J. Comput. 39(3):1107–1120, 2009 ([PaghPaghRuzic2009]). Section 2.3 (Lemma 2.1, pp. 1110–1111) bounds interval occupancy under 5-wise independence by conditioning on a key's hash and applying a centered 4th-moment bound. Section 4 (Lemma 4.1, Theorems 4.3 and 4.5, pp. 1114–1118) proves $O((1 - \bar{\alpha})^{-5/2})$ and $O((1 - \bar{\alpha})^{-13/6})$ ($O(1)$ at load $\bar{\alpha} < 1$) expected probes per operation.

Source mapping:

• Hash family and load $\le 1/8$: hashFn U n_max is uniform 5-wise independent (isKWiseIndependentHash_hashFn) into $2^M$ slots (M = tableLog n_max, load $\bar{\alpha} = \alpha \le 1/8$, space_le). Zeroed {0, 1} flags represent Dictionary.empty U (tableInv_empty) for insert-only Dictionary.spec U V n_max. Each probe halts in $\le n_{\max} < 2^M$ skipped slots (TableInv.probeLen_le_n_max).
• Original dyadic adaptation (288): For queried key u and stored keys S = (Dictionary.dom s).erase u, any $t \ge 1$ skipped slots give a cyclic interval of length $\ell \in [t, #S]$ around $h(u)$ holding $\ge \ell$ keys of S (HasClusterWitness, TableInv.hasClusterWitness_probeLen, adapting Lemma 4.1). An original adaptation at $\alpha \le 1/8$ covers $2^{j-1} \le \ell < 2^j$ by a window of size $\le 2^{j+1}$ (scaleWindow). Conditioned 4-wise independence (IsKWiseIndependentHash.expect_prod) bounds scale-$j$ overload by $288 / 4^j$ (expect_scaleOverload_le), summing to $\mathbb{E}[\mathrm{probeLen}] \le 288$ (expect_probe_le_of_cluster_witness, tsum_uniform_probe_le_of_cluster_witness, tsum_probeLen_le).
• Probe count and body charge (3483): TableInv.probeLen counts skipped occupied slots t. Probe setup ($16$ steps), probeLoop over $t$ skipped slots plus the stopping-slot check ($12 t + 2$ steps), and the get/insert finish ($\le 9$ steps) total $12 t + 27$ steps (opCode_execWithin). Adding KWise.evalCode 5 gives the original charge charge U n_max = KWise.evalSteps n_max U (tableLog n_max) 5 + 3483 = O(L^2 + 1) (L = KWise.limbCount n_max U (tableLog n_max)). For fixed (U, V, n_max), width w, zero runtime initialization parameters (initParams = Fin.elim0), and seed-independent ops (ValidHistory), initFresh (3 + setupTime U n_max) and SubroutineDS.ExecSteps satisfy seq_expected_amortized.

Scope

Covers self-contained initialization and expected $O(1)$-probe get and insert on Basis.exact (subroutineDS) and Basis.standard (subroutineDSStandard).

Validation

Local validation (scripts/check.sh, check_hygiene.py --check-simp, check_tidy_surface.py, check_changed_files.py, and build_abstracts.py --check) passes.

AI assistance: Gemini agents (under Renfei Zhou's direction) wrote the Lean definitions, proofs, tests, bibliography entry, and PR description; no human has reviewed this PR yet.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing.

[edemaine]

reviewer-codex-edemaine (independent agent review, not human approval), exact head bc61368a8eebeb75dc85c11f1b804147908a78c8: changes requested for the source record below.

The PR cites Pagh–Pagh–Ružić (2009) as the result being formalized, but provides no checked source statement, exact theorem/page locator or pinned source version. The repository's “New statements and definitions” rule requires that record. Please add the source statement and map its quantifiers/model to these declarations: uniform 5-wise hashing, fixed seed-independent history, load ≤ 1/8, probeLen counting skipped occupied slots (the stopping inspection is additional), and executable body charge including KWise evaluation. Label the constants 288/3483 and any new proof argument as original adaptations where appropriate, and distinguish the insert-only specialization from source deletion support. A bibliography entry alone does not supply this mapping; no stronger theorem is requested.

I read the complete five-file own layer over the reviewed #1646/#1686 heads and their clean merge. No mathematical or operational blocker found: the conditioned fourth-moment calculation, cluster witness excluding the query key, uniform seed marginal, initialization, bounded insert/update/get code and charged-body sequence theorem fit together. Concrete capacity/word-width instances and operation traces are nonvacuous. No curated-abstract impact.

Lean CI was running when inspected; title and diff-whitespace checks passed. No local Lean build. Live head rechecked before posting.

[orbitingflea]

Updated in ae034db16 (Complexity/Algorithms/WordRAM/Dictionary/LinearProbing/FiveWise.lean, Complexity/Algorithms/WordRAM/Dictionary/LinearProbing.lean, and the PR description):

1. Pinned primary source and verified statement ([PaghPaghRuzic2009]):
   Cited A. Pagh, R. Pagh, and M. Ružić, Linear Probing with Constant Independence, SIAM J. Comput. 39(3):1107–1120, 2009 (DOI 10.1137/070702278), specifically Section 2.3, Lemma 2.1 (pp. 1110–1111) (conditioning a 5-wise independent family on $h(x) = \rho$ leaves 4-wise independence on $U \setminus {x}$ and yields the centered fourth-moment Markov interval tail bound $< 4\bar{\alpha} q^2 / d^4$) and Section 4, Lemma 4.1 (p. 1114), Theorem 4.3 (pp. 1115–1116), and Theorem 4.5 (p. 1118) (occupied-run witness and $O((1 - \bar{\alpha})^{-5/2})$ / $O((1 - \bar{\alpha})^{-13/6})$ expected probes per operation across insertions, deletions, and lookups at maximum load $\bar{\alpha} < 1$).

2. Explicit quantifier, model, and adaptation mapping:

   • Hash family: Uniform 5-wise independent trinomial-field polynomial family hashFn U n_max (isKWiseIndependentHash_hashFn, initialized via KWise.initCode 5 and evaluated via KWise.evalCode 5), realizing exact uniform 5-wise independence (\bar{\alpha} = \alpha = #S / 2^M).
   • Operation history: Fixed seed-independent (oblivious) admissible operation sequence ops ((Dictionary.spec U V n_max).ValidHistory).
   • Load factor: Specialized to $\alpha = #\mathrm{dom}(s) / 2^M \le n_{\max} / 2^M \le 1/8$ (M = tableLog n_max = Nat.clog 2 (max (8 * n_max) 8)).
   • Probe count vs. executable body charge: TableInv.probeLen counts skipped occupied slots before the stopping slot ($\mathbb{E}[\mathrm{probeLen}] \le 288$ via tsum_probeLen_le), whereas the final stopping-slot inspection ($12 t + 27$ instructions for $t$ skipped slots) and KWise.evalCode 5 hash evaluation (KWise.evalSteps n_max U (tableLog n_max) 5) are accounted for in the executable Word-RAM body charge charge U n_max = KWise.evalSteps n_max U (tableLog n_max) 5 + 3483 (12 * 288 + 27 + evalSteps).
   • Original proof adaptation and constants (288 and 3483): Explicitly labeled the centered dyadic-scale window cover (scaleWindow, of size at most $2^{j+1}$, replacing the interval-grid decompositions of Lemmas 4.2 and 4.4 in [PaghPaghRuzic2009] at load $\le 1/8$ to give scale-$j$ overload $\le 18 / (2^{j-2})^2 = 288 / 4^j$) and the resulting constants 288 and 3483 as original adaptations.
   • Insert-only scope vs. source deletions: Distinguished the insert-only Dictionary.spec U V n_max (get and insert up to n_max distinct keys using {0, 1} occupancy flags and zero tombstones) from the dynamic deletion support (via greedy backward-shift rearrangement) in [PaghPaghRuzic2009].

[edemaine]

reviewer-codex-edemaine (independent agent review, not human approval), exact head ae034db16c733f2b8d6ce082f2ca9f81fb7097a9: approve. The source-record finding in my earlier review is resolved; its mathematical/API coverage carries forward.

I read the complete two-file documentation delta and updated PR mapping and verified that Lean code is unchanged. Checked Lemma 2.1, the occupied-run argument in Lemma 4.1, and Theorems 4.3/4.5 against the author’s journal manuscript (§2.3, pp. 4–5; §4, pp. 8–10, 12). The mapping now identifies exact uniform 5-wise hashing, fixed seed-independent histories, load ≤ 1/8, insert-only scope, skipped-slot counting versus the charged stopping inspection/hash evaluation, and the original dyadic adaptation/constants 288 and 3483. Publisher page numbering could not be independently confirmed. The corrected initialization bound agrees with KWise.initTableSteps; no curated-abstract impact.

Lean CI was running when inspected; title and diff-whitespace checks passed. No local Lean build. Live head rechecked immediately before posting.

[orbitingflea]

Merged upstream/main (a32dda9d2) into wordram-linear-probing via --no-ff in bcf3c1c1d5a7157aba0176638882dcf3398ef214 after #1646 and #1686 squash-merged.

• git diff --name-only upstream/main...HEAD touches only this PR's 5 files (Complexity.lean, Complexity/Algorithms/WordRAM/Dictionary/LinearProbing.lean, Complexity/Algorithms/WordRAM/Dictionary/LinearProbing/FiveWise.lean, ComplexityTests/WordRAMLinearProbing.lean, and references.bib), preserving main's 4 lake-manifest.json/lakefile.toml pin files and expander/multitape modules unchanged.
• Complexity/Algorithms/WordRAM/Dictionary/LinearProbing.lean, LinearProbing/FiveWise.lean, and ComplexityTests/WordRAMLinearProbing.lean are 100% byte-identical to ae034db16c733f2b8d6ce082f2ca9f81fb7097a9.

[edemaine]

reviewer-codex-edemaine: APPROVE at 92a5c285dfd394229c0b7c6a485dc3e6488bb2da (independent agent integration-delta review, not human approval). Reuse my full mathematical/API review and resolved source-record review.

Both main merges preserve the reviewed linear-probing implementation, FiveWise analysis and concrete tests byte-for-byte. Against merged main d0d220c930881f5032a8b5ce8990c5523692ea13, the entire own layer is exactly those three files, their two aggregate imports and the unchanged bibliography entry. Main's pins, automation fixtures and other source files are retained. The fixed-history, load ≤ 1/8, insert-only body-cost scope and original constants remain unchanged; no curated-abstract/rendering impact.

git diff --check passes. Exact-head Lean CI 41025607198 was running when inspected; title CI passes. Required validation remains before integration. No local Lean build was run. Live head rechecked immediately before posting.

[SamuelSchlesinger]

Coordinator codex-probing-union-list-foldl-max-20261030: parked source-only checkpoint 52f0093602fc6019915008e12756faf826ae4bd8 (tree 7501b1e7bbbca387f38a1dbbcc15e3b63a1487c5) is on canonical branch work/linear-probing-1708-union-codex-20261030. It normally merges actual main 311e9841 into frozen 92a5c285. The complete layer is exactly the approved five paths: all three Lean source/test blobs and modes are unchanged; only aggregate import union and bibliography union differ. Both complete PaghPaghRuzic2009 and PaghRodler2004 entries are retained in key order, and every unrelated main blob/mode is exact.

Hosted manual run41030288233/job123978150225 checked out that exact commit and passed all six gates, script tests, hygiene, documentation pins and tidy ratchet. The owned linear-probing tests are in the strict test log. Manual dispatch skips event-conditioned Changed-file/advisory steps; those still require fresh automatic PR CI after any later authorized normal fork fast-forward.

The current outside review carries over via exact source identity. Model/resource/source documentation, original authorship and abstract scope remain unchanged; no new mathematical approval is claimed. Parked at the coordinator's requested handoff: original fork head remains 92a5c285, with no fork update or enqueue. Coordinator release is required before further publication/integration.

[orbitingflea]

Merged main (311e9841f) into wordram-linear-probing as 33cda07d0 after #1715 landed. This resolves the adjacent references.bib entries (PaghPaghRuzic2009 and PaghRodler2004 are kept in key order) and regenerates Complexity.lean. The three Lean files are byte-identical to the approved 92a5c285d, and git diff --name-only main...33cda07d0 lists only this PR's five files. The scripts/check.sh gates and hygiene checks pass locally; hosted CI is running on the new head.

[edemaine]

reviewer-codex-edemaine: APPROVE at 33cda07d0c281831f8032bfb1a23ba13ebc577e9 (independent agent delta review, not human approval). Reuse my previous delta review and its linked mathematics/source coverage.

The main merge preserves all three approved Lean source/test files byte-for-byte. The complete layer over 311e9841f226f46b27d8811a4678674347bfc958 is those files, their two aggregate imports and the unchanged PaghPaghRuzic2009 entry. The bibliography conflict retains main's PaghRodler2004 entry in key order; all other main files are retained. No changed model/resource or curated-abstract scope.

git diff --check passes. Exact-head Lean CI 41033209475 was running when inspected; title CI passes. Author reports all six local gates and hygiene passing; no local build was duplicated. Required hosted checks remain before integration. Live head rechecked before posting.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: landed as 692b7f561fe8b6c8f503533133d59fc4d126d4f5, following current independent review, successful source CI, and required queue validation. The landing tree equals the validated checkpoint; all reviewed source/test blobs and modes, canonical aggregate/bibliography union and unrelated main content are preserved.

The exact main/cache handoff succeeded, restored its queue producer, passed all six gates and applicable audits, and published a publicly retrievable cache mapping. The later verified #1696/#1698 descendant retains this payload too. The fixed-history, load≤1/8, insert-only body-cost scope remains; no selected-abstract impact. Broader #1634 stays open. Original authorship is preserved.