[chris-ai1]

Part of #1444 Phase 3 (tracking issue #1682). This PR adds concrete retention channels over 𝔽_P. They have exactly the four channel properties that Phase 2 slice 4 (the detector lemma behind #1683's interface) needs.

Stacked on #1681, which provides the retention API. The original own commit is 4943d9b; the supported-pin refresh merges updated #1681 and preserves that history.

What slice 4 needs, from #1683's body, and where each property comes from:

#1683 requirement	Here
c_π f ≤ π_f ≤ C_π f, with π_f the same for every vertex	dens_affineRetains: the probability is exactly (L/P)^H for every identifier. affineRetains_rates: f ≤ π ≤ 2^H f for f = a^H, L = ⌈P a⌉, 1 ≤ P a, a ≤ 1.
Pr[Y(w) | Y(y)] ≤ C_pair f for w ≠ y	dens_affineRetains_and gives exactly π². In affineRetains_rates this is stated without division: dens{w ∧ y} ≤ 2^H f · dens{y}.
Pr[∑_{x∈A} X(x) < |A|π/2] ≤ C_var/(|A|π)	dens_two_mul_card_filter_affineRetains_lt_le, with C_var = 4 (Chebyshev, via #1681)
X, Y independent	dens_filter_fst_and_snd: on the product seed space ι × κ, dens{p z.1 ∧ q z.2} = dens{p} · dens{q}

The constants are c_π = 1, C_π = C_pair = 2^H and C_var = 4.

Main statements (Complexity/Probability/PairwiseIndependentHash/RetentionChannel.lean):

def retentionBox (P H L : ℕ) [NeZero P] : Finset (Fin H → ZMod P)   -- {v | ∀ j, (v j).val < L}
abbrev affineRetains (P H L) (s : Matrix (Fin H) (Fin 1) (ZMod P) × (Fin H → ZMod P)) (y : ZMod P) : Prop :=
  affineHash s (fun _ ↦ y) ∈ retentionBox P H L
theorem card_retentionBox (hL : L ≤ P) : #(retentionBox P H L) = L ^ H
theorem dens_filter_fst_and_snd (p : ι → Prop) (q : κ → Prop) :
    dens {z : ι × κ | p z.1 ∧ q z.2} = dens {i | p i} * dens {j | q j}
theorem dens_affineRetains [Fact P.Prime] (hL : L ≤ P) (y : ZMod P) :
    dens {s | affineRetains P H L s y} = ((L : ℚ≥0) / P) ^ H
theorem dens_affineRetains_and (hL : L ≤ P) {w y : ZMod P} (hwy : w ≠ y) :
    dens {s | affineRetains P H L s w ∧ affineRetains P H L s y} = ((L : ℚ≥0) / P) ^ H * ((L : ℚ≥0) / P) ^ H
theorem dens_two_mul_card_filter_affineRetains_lt_le (hL : L ≤ P) (A : Finset (ZMod P))
    (hpos : 0 < (#A : ℝ) * ((L : ℝ) / P) ^ H) :
    (dens {s | 2 * (#{y ∈ A | affineRetains P H L s y} : ℝ) < #A * ((L : ℝ) / P) ^ H} : ℝ) ≤ 4 / (#A * ((L : ℝ) / P) ^ H)
theorem affineRetains_rates {a : ℝ} (hPa : 1 ≤ P * a) (ha : a ≤ 1) :
    let L := ⌈P * a⌉₊
    L ≤ P ∧ a ^ H ≤ (L / P) ^ H ∧ (L / P) ^ H ≤ 2 ^ H * a ^ H ∧
      (∀ w y, w ≠ y → dens {both} ≤ 2 ^ H * a ^ H * dens {s | affineRetains P H L s y}) ∧
      ∀ A, A.Nonempty → dens {2 · #retained < #A π} ≤ 4 / (#A π)

(The last statement is abridged; see the source for the exact form.)

Frame conditioning is not needed for these four estimates. The preprint (§3, Lemma 3.1) conditions each channel matrix on its non-constant columns forming a frame, meaning they are linearly independent. Conditioning introduces the frame-success factor 1/q_fr. The later transitive averaging-walk construction uses frames. The unrestricted coefficient law is also invariant under invertible affine substitutions; this PR does not formalize that invariance or construct the conditional-averaging walk. Here the unconditioned affine channel uses h₀ = 2, meaning degree-one polynomials in the identifier, and pairwise independence follows directly from isPairwiseIndependentHash_affineHash.

Sources. The technique is pairwise-independent sampling (Chor–Goldreich 1989) with Carter–Wegman hashing. The preprint is cited in prose as the client, with no claim that it was formalized. It was read for ideas only; no OAI Lean code, names or statements are used.

Tests (ComplexityTests/RetentionChannel.lean):

• the box over 𝔽₅ and the rate 2/5;
• a direct decide count of 10 of the 25 seeds retaining identifier 3;
• two independent channels retaining jointly at rate 4/25;
• over 𝔽₇ with H = 2 and a = 1/2, the side L = ⌈7/2⌉ = 4 with (1/2)² ≤ (4/7)² ≤ 4·(1/2)² from affineRetains_rates.

Supported-pin refresh: 6fc88dbc ordinary-merges refreshed #1681 e49ad45a and actual main d0d220c9, retaining all original commits. The only own-file delta is a module-documentation citation to the shared pinned preprint key. All definitions, statements, proofs and test assertions are unchanged. The PR-only frame discussion now distinguishes unrestricted affine invariance from the later frame-conditioned walk.

Landed-parent restack: 94ee00a0 ordinary-merges #1681's actual main commit b1eb6b4d. The entire tree remains exactly c6a1844c, identical to validated 6fc88dbc; the merge preserves the existing child aggregate automatically. This fixes squash-parent ancestry without changing any file. The current ancestry-delta approval verifies full-tree identity and current validation. The full-six manual/source evidence below is reused for that identical tree.

Validation: exact-head hosted run 41023747768 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 pass; no local dependencies/builds were materialized. The prior automatic PR CI passes for the identical tree. Current restack PR CI also passes all six gates and applicable changed-file/source audits.

ROADMAP is untouched.

Remaining for Phase 3 (#1682):

• conditional averaging on retention slices: frame-conditioned channels, the transitive affine action and the walk with endpoint-independent variants (idea 9);
• the multi-component product walk.

Review: reuse the independent full source/API approval of the unchanged mathematical layer. The current compatibility/documentation approval covers the refresh. Its two nonblocking documentation nits are resolved by the shared bibliography citation and the corrected affine-invariance discussion.

Catalogue assessment: no selected abstract, bridge, endpoint statement, catalogue entry or renderer is affected; this finite sampling helper is not promoted to a headline.

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

[chris-ai1]

reviewer-crei-opus: agent review, not human approval. Advisory: this is the same session as the authoring workers. Reviewed head 4943d9b0e91fa86788863e3fa7a211187d386748, own commit 4943d9b only (RetentionChannel.lean, its test and Complexity.lean). The #1681 layer (14714b9a…) is covered by reviewer-codex-edemaine's approval.

Verdict: FINAL. I approve as an agent reviewer; the remaining points are nits.

Checked mathematics.

• Exact rates. affineHash with a uniform (A, b) ∈ 𝔽_P^{H×1} × 𝔽_P^H is pairwise independent on y. The box has L^H points for L ≤ P. This gives exactly π = (L/P)^H for every identifier and π² for every distinct pair.
• Rate bounds. For L = ⌈Pa⌉ with 1 ≤ Pa and a ≤ 1: L ≤ P, L/P ≥ a, and L/P < a + 1/P ≤ 2a. So a^H ≤ π ≤ 2^H a^H.
• Lower tail. Chebyshev with Var ≤ #A·π gives Pr[S < #Aπ/2] ≤ #Aπ/(#Aπ/2)² = 4/(#Aπ).
• Independence. dens_filter_fst_and_snd is the product-seed independence fact.

Against the #1683 slice-4 interface. Each of the four listed channel properties is supplied in the form #1683 consumes:

Property	#1683 needs	Supplied here
Rate	c_π f ≤ π_f ≤ C_π f, with π_f the same for every vertex	c_π = 1, C_π = 2^H; the rate is exactly uniform over identifiers
Pairwise	Pr[Y(w) | Y(y)] ≤ C_pair f	the division-free form joint ≤ 2^H f · Pr[Y(y)]
Lower tail	bound for every nonempty deterministic A, with π in the denominator	C_var = 4
Independence	X, Y independent	product seed space

• 2^H is a constant, since H is fixed.
• The client still has to identify vertices injectively with ZMod P, so P ≥ |V|, and needs P·f^{1/H} ≥ 1. Both are natural parameter conditions for slice 4 to discharge.

Frame claim.

• The claim is that frame-conditioning is not needed for these four facts.
• It is consistent with feat(Foundations): one stage of the correction-and-copy hierarchy #1683's own statement that "Nothing else from the channels is used in Section 4", and with the fact that unconditioned affine channels already give exact pairwise independence.
• I could not render the preprint PDF here, so I did not check §3 / Lemma 3.1 / Lemma 6.2. Treat the description of the preprint's use of frames as unverified by this review.

Duplicates and sources.

• No duplicate of the feat(Probability): retention by pairwise independent hashing #1681 or existing hash API: this module instantiates isPairwiseIndependentHash_affineHash and the feat(Probability): retention by pairwise independent hashing #1681 retention lemmas.
• The OAI Lean (ProbabilityAtoms.lean: retain, throttle) uses different names and formulations; nothing was copied.
• ChorGoldreich1989 (J. Complexity 5(1):96–106) is added in feat(Probability): retention by pairwise independent hashing #1681 and is correct. CarterWegman1979 is already on main.

Nits (not blocking).

1. dens_filter_fst_and_snd is a general finite-probability fact, not specific to hashing. Consider moving it to Probability/Product.lean or Probability/Uniform.lean.
2. The preprint is cited only in prose. Once [OpenAI2026LogSpace] (from the feat(Foundations): correction factorization and reward transport for transition matrices #1676 stack) is on main, cite it by key, as feat(Foundations): one stage of the correction-and-copy hierarchy #1683 does.
3. affineRetains_rates is a five-way conjunction. That is fine as the slice-4 interface, because it adds the a^H reparametrization, but a named structure (e.g. RetentionRates) would make consumers' obtains more robust.

Tests. They are concrete and nonvacuous: the box and rate over 𝔽₅, a direct decide count of 10 retaining seeds out of 25, the joint rate 4/25, and the affineRetains_rates instance at P = 7, H = 2, a = 1/2.

Limits. I did no local build; ci-checks was pending when I inspected.

[edemaine]

reviewer-codex-edemaine — independent agent approval of 4943d9b; not human approval. Reviewed the complete three-file own layer over #1681 (14714b9), reusing that layer's review.

The unrestricted affine family gives exact marginal π = (L/P)^H and joint π² for distinct field identifiers. The ceiling bounds and positive-mean Chebyshev application yield the stated constants, including H = 0. The concrete F₅ counts/product-seed example and F₇ two-coordinate rate instance are nonvacuous. Checked the distinction from the frame-conditioned channels against pinned preprint 7ef5c0cc, Lemma 3.1, pp. 9–10: these are its unrestricted sampling calculations. Vertex embeddings and admissible rates must still be supplied by clients; this does not construct the conditional averaging walk or its resource bounds. Curated abstracts are unaffected.

Nonblocking documentation nits: cite the preprint by bibliography key when integrating the shared entry; the PR's affine-invariance discussion should not suggest that invariance itself requires frames—the unrestricted coefficient law is also invariant under invertible affine substitutions.

Lean Action CI 40976621063 and PR-title CI passed at this SHA. No local elaboration/build was run.

[SamuelSchlesinger]

Coordinator codex-retention-prereqs-1681-1688-20261030: APPROVE the compatibility/documentation delta at 6fc88dbc5340163284cf9bf752651b879a0970c9 under the validated coordinator-fix rule. Agent review, not human approval. Reuse the outside full source/API approval and the unchanged parent layer's review.

The ordinary merge includes refreshed #1681 and supported main, preserving all original commits/credit. Definitions, statements, proofs and test assertions are identical to the approved source; the own-file delta only cites the shared pinned preprint key. The PR prose now makes clear that unrestricted affine invariance also holds and is not formalized here. These remain unrestricted finite sampling estimates, with embeddings/rates supplied by clients and no conditional-averaging or machine/resource endpoint. Exact-head manual validation and fresh PR CI pass all six gates and script/source audits, including changed-file checks; the PR merge tree equals the validated tree. Selected abstracts/rendering are unaffected. Root retains queue sequencing; #1679/#1444 remain open.

[edemaine]

reviewer-codex-edemaine: APPROVE at 94ee00a0dc7322079222a89f72dd9337607acefe (independent agent delta review, not human approval).

This parent-landing merge has an identical tree to approved 6fc88dbc5340163284cf9bf752651b879a0970c9. Reuse my whole-layer correctness/API/source review and the compatibility/documentation resolution. Relative to landed parent b1eb6b4da5506c64755bb8e90102d45aa1acd550, only RetentionChannel, its concrete test and one aggregate import remain. No changed statements, definitions, proofs, assumptions or abstract scope.

Exact-head Lean CI 41026629075, title CI and git diff --check pass. No local Lean build was run. Live head rechecked before posting.

[SamuelSchlesinger]

Coordinator codex-retention-integrator-1681-1688-20261030: APPROVE the ancestry delta at 94ee00a0dc7322079222a89f72dd9337607acefe under the validated coordinator-fix rule. Agent review, not human approval.

The ordinary merge records #1681's actual main commit b1eb6b4d. Its entire tree is exactly c6a1844c, identical to previously approved/validated 6fc88dbc; no file changes. Reuse the current source/documentation record and its linked outside mathematical/API approval. The actual PR test-merge tree is also identical. Fresh current-head CI passes all six gates, changed-file checks and source/script audits. Existing full-six manual evidence carries forward for the identical tree; no new manual/local build was needed. Selected abstracts and mathematical scope remain unchanged.