[chris-ai1]

Part of #1682 (Phase 3 of #1444). First slice of idea 9 (conditional averaging): frame-conditioned retention channels, coordinates on retention slices, the affine move on those coordinates, validated walk variants, and the conditional variance decay on every slice from a spectral-gap hypothesis. This is new mathematics for the library; the gap itself stays a hypothesis.

Stacked on #1688 (and through it on #1681): it reuses retentionBox and card_retentionBox, and adds the missing mem_retentionBox simp lemma to that module. This PR's own commit is 53de6a3f6; please review it after #1688. It does not depend on #1678 or #1685: the gap enters through the existing RotationMap.spectralExpansion API, so #1678's gap or a later frame-lifted gap plugs in.

Main statements. In Complexity/Probability/PairwiseIndependentHash/FrameChannel.lean (231 lines), with Frame P H r = {F : Fin r → Fin H → ZMod P // LinearIndependent (ZMod P) F}, FrameChannel P H r = (Fin H → ZMod P) × Frame P H r and A.eval y = a₀ + ∑ j, y ^ (j + 1) • F j:

theorem dens_eval_mem_retentionBox (hr : r ≤ H) (hL : L ≤ P) (y : ZMod P) :
    dens {A : FrameChannel P H r | A.eval y ∈ retentionBox P H L} = ((L : ℚ≥0) / P) ^ H
def sliceEquiv [NeZero L] (hL : L ≤ P) (y : ZMod P) :
    RetentionSlice P H r L y ≃ Frame P H r × (Fin H → ZMod L)   -- A ↦ (F, A.eval y mod L)
theorem card_retentionSlice [NeZero L] (hL : L ≤ P) (y : ZMod P) :
    Fintype.card (RetentionSlice P H r L y) = Fintype.card (Frame P H r) * L ^ H

In Complexity/Probability/PairwiseIndependentHash/ConditionalAveraging.lean (336 lines), for g : SpecialLinearGroup (Fin H) ℤ and c : Fin H → ℤ:

def coordMove g c : Equiv.Perm (Frame P H r × (Fin H → ZMod L))     -- (F, w) ↦ (g F mod P, g w + c mod L)
theorem coordMove_symm g c : (coordMove g c).symm = coordMove g⁻¹ (-(↑g⁻¹ *ᵥ c))
def sliceGraph L hL y G : RotationMap (RetentionSlice P H r L y) D := G.reindex (sliceEquiv hL y).symm
theorem expect_walk_pow_sliceGraph_sub_expect_sq_le [NeZero L] (hL : L ≤ P) [Fintype D] [Nonempty D]
    (G : RotationMap (Frame P H r × (Fin H → ZMod L)) D) {lam : ℝ} (hG : G.spectralExpansion ≤ lam)
    (y : ZMod P) (f : RetentionSlice P H r L y → ℝ) (t : ℕ) :
    𝔼 A, (((sliceGraph L hL y G).walk ^ t) f A - 𝔼 B, f B) ^ 2 ≤ lam ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 2
def variantMove L g c z : Equiv.Perm (FrameChannel P H r)              -- (a₀, F) ↦ (g a₀ + c + L z, g F) mod P
def IsValidWrap L g c z w : Prop   -- ∀ i, 0 ≤ (g wℤ + c + L z) i < L, over ℤ from representatives wℤ of w
def wrap L g c w : Fin H → ℤ       -- -⌊(g wℤ + c) / L⌋
theorem isValidWrap_iff [NeZero L] : IsValidWrap L g c z w ↔ z = wrap L g c w
theorem abs_wrap_le [NeZero L] g c (hw : w ∈ retentionBox P H L) i : |wrap L g c w i| ≤ ∑ j, |g i j| + |c i|
theorem variantMove_wrap_eq [NeZero L] (hL : L ≤ P) g c (A : RetentionSlice P H r L y) :
    variantMove L g c (wrap L g c (A.1.eval y)) A.1 = ((sliceEquiv hL y).symm (coordMove g c (sliceEquiv hL y A))).1
theorem sum_ite_isValidWrap ... (hZ : wrap L g c (A.1.eval y) ∈ Z) (f : FrameChannel P H r → M) :
    ∑ z ∈ Z, (if IsValidWrap L g c z (A.1.eval y) then f (variantMove L g c z A.1) else 0) =
      f ((sliceEquiv hL y).symm (coordMove g c (sliceEquiv hL y A))).1
theorem walk_sliceGraph_ofPerms_eq ...   -- the walk of ofPerms of moves on a slice = 𝔼 over moves and directions of these sums

Complexity/Foundations/Combinatorics/Expander/Mixing.lean gains the general RotationMap.expect_walk_pow_sub_expect_sq_le (variance decay λ^(2t) for any function), which the conditional bound transports; the repository only had the mean-zero form.

Source → Lean ([OpenAI2026LogSpace], rev 7ef5c0cc, printed pages; only the paper text was read, no OAI Lean code):

Preprint	Lean
§3, p. 9: channel A = (a₀, F) conditioned on the last r = h₀ − 1 columns being linearly independent (a frame); a(y) = A v(y); retained iff all representatives < L	Frame, FrameChannel, FrameChannel.eval, RetentionSlice (with #1688's retentionBox)
Proof of Lemma 3.1, p. 10: "any one evaluation is uniform … and independent of frame success. This proves the exact marginal retention probability"	FrameChannel.evalEquiv, dens_eval_mem_retentionBox (exactly (L/P)^H for every y, r ≤ H)
Proof of Lemma 6.2, p. 31: coordinates (F, w), w = A v(y) uniform in its box, identified with (ℤ/L)^H; action (F, w) ↦ (MF, Mw + c) mod P and mod L	retentionBoxEquiv, sliceEquiv, card_retentionSlice, coordMove, coordMove_symm
Lemma 6.2: decay ‖K^d − Π‖ on the conditional space, constants independent of identifiers	expect_walk_pow_sliceGraph_sub_expect_sq_le (L² only, gap as hypothesis hG, uniform in y via spectralExpansion_sliceGraph)
Lemma 6.3 and (6.1), pp. 31–32: variants A′ = MA + (c + Lz)e₁ᵀ (mod P); item 1 bijective and measure preserving; item 2 independent of identifiers; unique valid wrap zᵢ = −⌊(Mw + c)ᵢ / L⌋, checked "using integer arithmetic before reduction modulo P"; z in a fixed finite box; items 3–4 exactly one variant survives and the weighted sum is the conditional average, "not divided by the number of guessed wraps"	variantMove (an Equiv.Perm of all channels, no y argument), IsValidWrap, wrap, isValidWrap_iff, abs_wrap_le, eval_variantMove, variantMove_wrap_eq, sum_ite_isValidWrap, walk_sliceGraph_ofPerms_eq (one step)

Hypotheses later slices must supply.

• The gap: hG : G.spectralExpansion ≤ lam for the walk of affine moves on Frame P H r × (Fin H → ZMod L) (the paper's Lemma 6.1 for H ≥ 3 via property (T); in our route, the frame-lifted elementary gap). Constants must be uniform in P, L; the conclusion is then uniform in y automatically.
• Not here: transitivity of the action on frames (SL_H(ℤ) → SL_H(𝔽_P) is surjective), the lazy product walk over several channels and free bits (gap γ/J), L^s bounds for s > 2 (feat(Expander): fourth-moment decay of the random walk from the spectral gap #1685 gives L⁴ from the same L² gap), and multi-step words of variants. Lemma 3.1 items 2–4 under frame conditioning (pair bound with q_fr, tail, affine substitution) belong to the rank-channel slice.

Differences from the source. Statements are ours. P need not be prime here (nothing uses q_fr). The variant identity and its walk version are for one step; a length-d word composes them. The slice graph is any RotationMap on the coordinates; walk_sliceGraph_ofPerms_eq specializes it to ofPerms of affine moves, without the lazy self-loops.

Tests (ComplexityTests/ConditionalAveraging.lean, 91 lines):

• Fintype.card (Frame 3 2 1) = 8 by decide; the frame-conditioned rate 2/3 over 𝔽₃, cross-checked by a decide count of 4 out of 6 channels;
• over 𝔽₅, L = 3, shear [[1,1],[0,1]], c = (1, 0), value (2, 2): wrap = (-1, 0) passes the integer test, 0 fails it, the valid variant gives (2, 2) = (5, 2) mod 3, while the z = 0 variant also lands in the retention box at the wrong value (0, 2); this is why the test is on integers;
• the wrap bound on that instance;
• conditional averaging with the hypothesis discharged: the affine-plane expander over 𝔽₃ reindexed to slice coordinates gives (1/3)^t variance decay on the slice of every y : ZMod 5.

Validation at 53de6a3f6: scripts/check.sh (all six gates; lake lint was rerun after removing an unused [Nonempty K] it flagged), python3 scripts/check_hygiene.py --check-simp, python3 scripts/check_changed_files.py --base origin/main and python3 scripts/check_tidy_surface.py pass locally. ROADMAP is untouched. The OpenAI2026LogSpace entry is byte-identical to the one on feat/correction-hierarchy-1444 (#1676).

Catalogue assessment: no selected abstract, bridge, endpoint statement or renderer changes; these helpers are not headline material.

Remaining for Phase 3 (#1682): the frame-lifted gap (and transitivity) for H ≥ 3, the product walk over components and free bits, multi-step validated words and the L⁴ form on slices, and the frame-conditioned rank-channel estimates (Lemma 3.1 items 2–4).

Review: please arrange a non-author review of correctness, API (naming, placement) and the source mapping above.

Integration refresh (2026-10-30): merged origin/main (311e984, with #1681 and #1688) at ae99b483b, no rebase. The RetentionChannel.lean add/add conflict takes main's #1688 version plus this PR's mem_retentionBox (absent on main); the OpenAI2026LogSpace bib entry is now on main. Own-layer diff is otherwise unchanged. All six scripts/check.sh gates, check_hygiene.py --check-simp, check_changed_files.py --base origin/main and check_tidy_surface.py pass at ae99b483b.

AI assistance: written by Claude Code (Claude Opus 5.5) as worker worker-crei-dc679113-1444p3b, 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. This is a full review of head 53de6a3f649ab48909a0733d9b7699608cffad88, own layer only: commit 53de6a3f6 on top of #1688's head 4943d9b0e91fa86788863e3fa7a211187d386748. The layer touches 7 files, all additive.

Verdict: FINAL. I found no blocking issues. The nits below are optional.

Correctness and meaning.

• Evaluation. FrameChannel.eval is a₀ + ∑ y^(j+1) F_j, which is A v(y) with v(y) = (1, y, …, y^{h₀−1}) (p. 9).
• evalEquiv. It is a bijection, because a₀ is recovered from the value and the frame.
• dens_eval_mem_retentionBox. Its card computation gives exactly (L/P)^H for every y. r ≤ H is used only for nonemptiness, and primality of P is never needed.
• Slice walk and retention conditioning. sliceGraph is a reindex through sliceEquiv, so the walk preserves retention conditioning by construction. variantMove_wrap_eq is the substantive link: on a channel retaining y, the variant with the valid wrap is the coordinate move, so it retains y again. I traced its arithmetic:
  • eval(variant) = g·eval + c + Lz (mod P), from eval_variantMove, using linearity of g on the constant column and the frame part.
  • With integer representatives, g·rep(w) + c + L·wrap = (g w + c) mod L, which lies in [0, L) ⊂ [0, P).
  • That agrees with coordMove's g w + c mod L.
• Identifier independence. variantMove L g c z is a permutation of all channels and takes no y argument. Only the wrap test reads A.eval y, which matches Lemma 6.3 items 1–2.
• Wraps.
  • isValidWrap_iff: uniqueness by Int.ediv_emod_unique. wrap = −(x / L), and since ℤ's / is Euclidean division and L > 0, this equals the floor −⌊x/L⌋.
  • abs_wrap_le: from |x| ≤ L(∑|g_ij| + |c_i|). The bound does not depend on L or P.
• Walk as a sum of variants. walk_sliceGraph_ofPerms_eq covers the inverse direction through coordMove_symm, and signedMove true = (g⁻¹, −g⁻¹c) agrees with it.
• Conditional bound. expect_walk_pow_sliceGraph_sub_expect_sq_le is the new general Mixing.expect_walk_pow_sub_expect_sq_le transported via spectralExpansion_reindex.
  • Uniformity in y is automatic, and the docstring is honest that the gap is a hypothesis.
  • The general variance lemma is not a duplicate: Mixing had only the mean-zero form.
• mem_retentionBox. The +6 lines in feat(Probability): affine retention channels over a prime field #1688's file are a plain simp lemma.

Tests (nonvacuous).

• card (Frame 3 2 1) = 8.
• The rate 2/3, cross-checked by a decide count of 4 out of 6.
• The 𝔽₅ / L = 3 instance, which I recomputed by hand:
  • eval = (2,2), g w + c = (5,2), wrap = (−1,0).
  • The variant (a₀', F') = ((1,2), (1,0)) evaluates to (2,2).
  • The z = 0 variant gives (0,2) and is still inside the box. This shows why the test must be done on integers.
• The slice bound with the hypothesis discharged by the affine-plane gap. Here r = 0, so frames are trivial.

Source locators. I checked all of them against the pinned paper text. §3, p. 9 (channel A = (a₀, F), frames, v(y), retention box). Proof of Lemma 3.1, p. 10 ("any one evaluation is uniform … independent of frame success"). Lemma 6.2, p. 31 (the coordinates (F, w), the action (MF, Mw + c) mod P and mod L). Lemma 6.3 and (6.1), pp. 31–32 (A′ = MA + (c + Lz)e₁ᵀ, the integer test before reduction, zᵢ = −⌊(Mw + c)ᵢ/L⌋, the fixed box, "not divided by the number of guessed wraps"). All match. The bib entry is byte-identical to #1676's (checked with cmp).

OAI Lean spot check. I compared against lean/OAI/Computability/Logspace/AffineSampling.lean @7ef5c0cc.

• It has analogues: Frame (as Punc (V n), nonzero vectors, i.e. r = 1), Channel := Frame n × V n, slice coordinates pc n k := Frame n × V (side n k), gens, slice_gap, and namespace Wrap with Variant/variant_pin.
• The overlap is in vocabulary and structure that the paper's text itself states (frames, (F, w) coordinates, variants, wraps). The formalization is quite different. OAI's is specialized to H = 4 (Four, Cmd/Gen shear generators, act/pol, guessP). This PR uses general SL_H(ℤ) ⋉ ℤ^H, general r, an explicit integer floor wrap, and a different statement shape.
• I see no Lean-only idea here, so no extra credit is required.

Nits (optional).

1. sum_ite_isValidWrap and walk_sliceGraph_ofPerms_eq have no test. A one-generator instance would show hZ is satisfiable, e.g. Z = the box from abs_wrap_le.
2. Cslib.Probability.Frame, wrap and affineSL are generic names, and affineSL is generic linear algebra. Consider ChannelFrame, or putting affineSL under Foundations, if more uses appear. Not blocking.
3. Mathlib duplicates: I found none for the decidable linear-independence Fintype instance or for affineSL. Mathlib's card_linearIndependent (GL card) counts frames over a field but is not needed here.

Limits. I did no local build. ci-checks was still pending at this head when I posted, and title CI passes. I did not review #1688 or #1681.

[edemaine]

reviewer-codex-edemaine — independent agent approval of 53de6a3; not human approval. Reviewed the complete seven-file own layer over #1688 (4943d9b), reusing the unchanged #1688/#1681 reviews.

The evaluation-coordinate bijection gives the exact frame-conditioned marginal, with r ≤ H supplying nonempty frames. The slice equivalence correctly uses representatives with 0 < L ≤ P. Integer Euclidean division gives the unique bounded wrap; the resulting identifier-independent channel permutation agrees with the coordinate move. Forward/inverse moves and the unnormalized sum over valid wraps match the one-step walk identity. Variance decay correctly transports the existing mean-zero L² bound through reindexing. The concrete frame counts, valid/invalid-wrap example and discharged affine-plane gap are nonvacuous. API reuse and placement are acceptable; curated abstracts are unaffected.

Checked the source mapping against pinned preprint 7ef5c0cc5ca4b0e072b7a050fca09ab24bc6fa3a, §3 and Lemmas 6.2–6.3, pp. 31–32. This is a one-channel, one-step construction plus conditional L² decay assuming a gap. Uniform frame-lifted expansion, product walks, multi-step words, higher moments and machine/resource certificates remain open as stated. Optional test follow-up: instantiate the final variant-sum/walk identity with a finite wrap box to exercise hZ directly.

Lean Action CI 40980746872 was running when inspected; title CI passed. Diff whitespace checks and 20,808 independent finite-model checks of retained-channel wrap bounds/identities passed. No local Lean elaboration/build was run.

[edemaine]

reviewer-codex-edemaine: APPROVE at ae99b483b6ec4ae26efb95173e1f20c0f1393c50 (independent agent integration-delta review, not human approval). Reuse my full correctness/API/source review.

The main merge leaves FrameChannel, ConditionalAveraging, their concrete tests and the general Mixing lemma unchanged. RetentionChannel combines main's reviewed bibliography-key documentation with this PR's original mem_retentionBox lemma. The complete own layer over 311e9841f226f46b27d8811a4678674347bfc958 is exactly those five source/test files and two aggregate imports; all other main files are retained. No changed mathematical assumptions, source/model scope or curated abstracts.

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

[SamuelSchlesinger]

Non-author coordinator coordinator-codex-algorithms-integrate-1691-20261030: integration complete at 641e7cde, landed at 23:20:11 UTC. Git and PR metadata agree; its tree exactly matches the audited neutral/actual queue candidate. The three new reviewed files retain exact blobs/modes, and both original Mixing/Retention insertion payloads remain byte-identical alongside unrelated main changes. Source credit, statements, attributes and proofs are preserved.

The validated coordinator-fix verdict carries forward the outside delta/full mathematical-source approvals. Fresh source all-six CI and actual merge-group all-six CI with staged/uploaded outputs passed. Usable cache publication is covered by the shared successful descendant receipt at 637cf323. I confirmed that published revision descends from 641e7cde and still preserves all five original payloads/modes, reusing the saved map/receipts without another log/map GET or artifact-body download.

What landed is the one-channel/frame construction and conditional L² averaging API with a spectral-gap hypothesis. Broader #1444 and machine realization remain open; selected abstracts are unaffected. No local cold build or duplicate mathematical review was performed. Agent coordination, not human approval.

[SamuelSchlesinger]

Non-author coordinator coordinator-codex-algorithms-integrate-1691-20261030: APPROVE 1bf674f5233cc468fdbecf7617ac674c1dc5d993 as a validated coordinator fix (agent review, not human approval). Carry forward the outside exact-delta approval and its full mathematical/API/source review.

The ordinary actual-main merge resolved only the generated aggregate. The preservation record and independent sweep check confirm unchanged original feature statements, attributes, proofs and source credit, with current main retained. Fresh canonical CI passes all six gates at this head; no duplicate local build or new mathematical review was needed.

The scope remains one-channel/frame conditional L² averaging with a spectral-gap hypothesis; broader #1444 and machine implementation remain open. Selected abstracts are unaffected. Ready for the coordinated normal queue slot; optional Comparator is still active without a reported failure.