[chris-ai1]

Part of #1444, Phase 3, first slice (idea 5 of #474). This adds retention by pairwise independent hashing. A point x is retained by seed i when h i x ∈ B for a fixed target set B ⊆ Y.

What already existed.

• Complexity/Probability/PairwiseIndependentHash has IsPairwiseIndependentHash and its single-target cell-size moments (B = {y}).
• The affine, Toeplitz and shift families.
• KWiseIndependent/Polynomial has polynomial hashing over a finite field, which is k-wise and hence pairwise independent.

What was missing is the general target set B: retention at a rate p = #B / |Y| other than 1 / |Y|.

Main statements (Complexity/Probability/PairwiseIndependentHash/Retention.lean, namespace Cslib.Probability.IsPairwiseIndependentHash, with hh : IsPairwiseIndependentHash h):

theorem dens_filter_apply_mem (hh) (x : X) (B : Finset Y) :
    dens {i | h i x ∈ B} = #B / Fintype.card Y
theorem dens_filter_apply_mem_and_apply_mem (hh) {x₁ x₂ : X} (hx : x₁ ≠ x₂) (B₁ B₂ : Finset Y) :
    dens {i | h i x₁ ∈ B₁ ∧ h i x₂ ∈ B₂} = #B₁ / Fintype.card Y * (#B₂ / Fintype.card Y)
theorem expect_card_filter_apply_mem (hh) (S : Finset X) (B : Finset Y) :
    𝔼 i, (#{x ∈ S | h i x ∈ B} : 𝕜) = #S * (#B / Fintype.card Y)
theorem expect_card_filter_apply_mem_mul_sub_one (hh) (S) (B) :
    𝔼 i, (#{x ∈ S | h i x ∈ B} : 𝕜) * (#{x ∈ S | h i x ∈ B} - 1) =
      #S * (#S - 1) * (#B / Fintype.card Y) ^ 2
theorem expect_card_filter_apply_mem_sub_sq (hh) (S) (B) :
    𝔼 i, ((#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)) ^ 2 =
      #S * (#B / Fintype.card Y) * (1 - #B / Fintype.card Y)
theorem dens_le_abs_card_filter_apply_mem_sub_le (hh) (S) (B) {ε : 𝕜} (hε : 0 < ε) :
    (dens {i | ε ≤ |(#{x ∈ S | h i x ∈ B} : 𝕜) - #S * (#B / Fintype.card Y)|} : 𝕜) ≤
      #S * (#B / Fintype.card Y) / ε ^ 2
theorem dens_two_mul_card_filter_apply_mem_lt_le (hh) (S) (B)
    (hpos : 0 < (#S : 𝕜) * (#B / Fintype.card Y)) :
    (dens {i | 2 * (#{x ∈ S | h i x ∈ B} : 𝕜) < #S * (#B / Fintype.card Y)} : 𝕜) ≤
      4 / (#S * (#B / Fintype.card Y))

The module also has 𝕜-valued expect_boole_* forms of the first two statements.

Source mapping.

These are unrestricted pairwise-independent sampling estimates, following Chor–Goldreich's two-point sampling method on Carter–Wegman hash families. They supply the calculations used before frame conditioning in the proof of Lemma 3.1 of the OpenAI preprint; the full rank-channel lemma remains later Phase 3 work.

Checked source: OpenAI preprint, revision 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a, §3, proof of Lemma 3.1, printed p.10, second paragraph, opening clause:

Without conditioning on a frame, two evaluations at distinct field points are independent uniform vectors

The source's evaluations correspond here to h i x, with uniform seed i, distinct inputs x₁ ≠ x₂ and target sets B₁, B₂. The abstract hash predicate supplies uniformity and pairwise independence; the F₅ polynomial family in the tests is a concrete instance.

• dens_filter_apply_mem gives the exact unrestricted marginal rate p = #B / |Y|. The paper additionally proves that conditioning preserves the marginal and compares it with its nominal rate; those arguments remain outside this slice.
• dens_filter_apply_mem_and_apply_mem gives the unrestricted joint equality p₁ p₂. Lemma 3.1 item 2 concerns a frame-conditioned conditional probability. The paper first bounds the frame-conditioned joint probability using the unrestricted product and the frame-success probability q_fr, then divides by the conditioned marginal. This PR supplies the product estimate, not those conditioning steps.
• The moments and dens_two_mul_card_filter_apply_mem_lt_le give the unrestricted variance/Chebyshev calculation on p.10, with lower tail 4/(#S·p). Conditioning introduces a factor 1/q_fr; that transfer is also later work.

Frame-conditioned channels, frame-success bounds, nominal-rate comparability and affine-substitution invariance remain in #1682. The preprint was read for ideas only; no OAI Lean code, names or statements were used. The bibliography adds ChorGoldreich1989 (J. Complexity 5(1):96–106), checked against Goldreich's publication list.

Tests (ComplexityTests/PairwiseRetention.lean) use polynomial hashing x ↦ c₀ + c₁x over 𝔽₅ with the box {0,1}:

• retention rate 2/5, cross-checked by a direct decide count of 10 retaining seeds out of 25;
• joint rate 4/25;
• mean count 2 over all five points.

Supported-pin refresh: e49ad45a ordinary-merges actual main d0d220c9, preserving the original 14714b9a commit and its library/test files byte-for-byte. All existing main files are preserved, with only the aggregate import and independent bibliography addition combined. No mathematical, public API or test changes are introduced.

Validation: exact-head hosted run 41023745470 passed all six gates and script/source audits on CSLib 254e30e6 / Mathlib 69552756 / Lean 4.36.0-rc2. Local source-only hygiene with the simp audit and documentation-pin checks also pass; no local dependencies/builds were materialized. Fresh automatic PR CI also passes, including changed-file checks. ROADMAP is untouched. This PR is independent of #1678.

Remaining for Phase 3:

• frame-conditioned channels and affine invariance;
• contraction in L⁴ (idea 8);
• conditional averaging on retention slices (idea 9).

Catalogue assessment: no selected abstract, bridge, endpoint statement or renderer changes. This sampling helper is not added to the headline catalogue.

Review: independent source/API approval covers the original source layer; its theorem and test text is unchanged in the supported-pin refresh. The current compatibility-delta approval covers the refresh. The source mapping above identifies the unrestricted proof ingredients and the remaining frame-conditioned construction.

Compatibility refresh: coordinator codex-retention-prereqs-1681-1688-20261030, using Codex. Original source credit is preserved.

AI assistance: written by Claude Code (Claude Opus 5.5) as worker worker-crei-dc679113-1444p3, for coordinator coordinator-crei-dc679113.

🤖 Generated with Claude Code

[edemaine]

reviewer-codex-edemaine — independent agent APPROVE at 14714b9a71fd012a55ca5605a15655c7830736a0, not human approval. Complete four-file own layer over 96fd02a85579bbbce97c02110ed80da02684cb2e.

The target-set formulas correctly extend the existing hash predicate: disjoint singleton events give marginal/joint retention, off-diagonal pairs give the factorial moment, and the variance yields the stated Chebyshev and half-mean bounds. The variance proof handles empty seed/domain cases; the lower-tail theorem explicitly requires positive mean. The polynomial-hash fixture checks rate 2/5, joint rate 4/25 and mean 2, with a direct 10-of-25 seed count.

Placement and reuse fit the existing uniform-density API. I checked the pinned preprint's Lemma 3.1 (pp.9–10) and the Chor–Goldreich bibliography/background against primary sources: these are unconditioned pairwise-independent estimates; frame conditioning, affine invariance and rank-channel construction remain outside this slice. No selected-abstract or machine/resource impact.

git diff --check passed. Current Lean CI 40973346150 and title checks passed; author reports all six local gates. No local Lean elaboration/build.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732 — PR-description/source-mapping correction complete at unchanged source 14714b9a71fd012a55ca5605a15655c7830736a0. Reuse the full independent approval; another full proof review is unnecessary. This is agent review, not human approval.

Supplemental non-authoring reviewer /root/review_bpl_containments_1666 confirmed the formulas, degenerate cases, positive-mean tail hypothesis and F₅ instance. We checked the pinned primary PDF at 7ef5c0cc, printed pp.9–10. The description now maps these lemmas to the unrestricted calculations in Lemma 3.1's proof, rather than claiming its frame-conditioned conditional-pair or lower-tail conclusions; frame transfer, nominal-rate comparability and invariance remain in #1682. I checked the fifteen-word quotation against the extracted primary text and its printed-page locator. No Lean source, selected abstract or rendering changes.

Exact-head CI passed. Supported-current-pin refresh and final integration checks remain required after the dependency migrations.

[SamuelSchlesinger]

Coordinator codex-retention-prereqs-1681-1688-20261030: APPROVE the compatibility delta at e49ad45a0fc9e125ae0ba77977e77b3b8cfb7d35 under the validated coordinator-fix rule. Agent review, not human approval. Reuse the outside full source/API approval and checked source-mapping record.

The ordinary main merge preserves original history/credit and the retention module/test byte-for-byte. Existing main files are retained; the aggregate and bibliography combine their independent additions. Definitions, statements, proofs, tests and mathematical scope are unchanged. Exact-head manual validation and fresh PR CI pass all six gates and script/source audits, including the applicable changed-file checks. The PR test-merge tree equals the validated source tree. Selected abstracts/rendering are unaffected; no local build outputs were created. This is readiness only: root retains queue sequencing, and #1679/#1444 remain open.