[chris-ai1]

Part of #1682 (Phase 3 of #1444). This is step (D) of the frame-lifted gap plan posted on #1682. It assembles the coordinate-pair bound (#1699) and the frame Poincaré inequality (#1703) into a spectral gap for the walk of affine moves on slice coordinates Frame P H 1 × (Fin H → ZMod L). The gap is uniform in P and L, and it discharges #1691's hypothesis hG. This is new mathematics for the library: an elementary replacement, for frames of length one, of the paper's property (T) input.

Stack. The branch feat/slice-gap-1444 merges three open PRs, each by a merge commit (no rebases):

• feat(Expander): Poincaré inequality for elementary moves on the nonzero vectors of (ZMod P)^H #1703 (feat/frame-gap-1444, head 0e293465b), which is on feat(Expander): Efron–Stein and the coordinate-pair bound for shears and translations #1699 → feat(Expander): relative Poincaré inequality for shears and translations with a spectator #1695 → feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678;
• feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691 (feat/conditional-averaging-1444, head 53de6a3f6), which is on feat(Probability): affine retention channels over a prime field #1688 → feat(Probability): retention by pairwise independent hashing #1681;
• feat(Expander): spectral gap of box products of permutation multigraphs #1693 (feat/box-product-poincare-1444, head a9e19a53a), which is on feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678.

All of them already contain origin/main (0ba8b2e59), and the merges were clean. This PR's own layer is commit bc81c6ab3; please review only that commit, after the lower PRs. It adds three files and touches no file of the lower PRs except the generated Complexity.lean.

Main statements.

Complexity/Foundations/LinearAlgebra/Matrix/Transvection.lean (58 lines). Mathlib already has Matrix.SpecialLinearGroup.transvection, which is reused; this file adds its action on all vectors (Mathlib only has the action on basis vectors) and compatibility with change of rings:

theorem Matrix.SpecialLinearGroup.map_transvection (f : R →+* S) (h : i ≠ j) (c : R) :
    map f (transvection h c) = transvection h (f c)
theorem Matrix.SpecialLinearGroup.transvection_mulVec (h : i ≠ j) (c : R) (v : n → R) :
    (transvection h c : Matrix n n R) *ᵥ v = update v i (v i + c * v j)

Complexity/Probability/PairwiseIndependentHash/SliceGap.lean (415 lines, namespace Cslib.Probability):

def Frame.equivNeZero [Fact P.Prime] : Frame P H 1 ≃ {v : Fin H → ZMod P // v ≠ 0}
theorem Frame.card_one [Fact P.Prime] : Fintype.card (Frame P H 1) = P ^ H - 1
theorem Frame.mapSL_transvection_apply_zero (h : a ≠ b) (F : Frame P H 1) :
    (Frame.mapSL (SpecialLinearGroup.transvection h 1) F).1 0 = RotationMap.elementaryMove a b (F.1 0)
theorem exists_expect_sq_sub_le_mapSL_transvection [Fact P.Prime] (hH : 3 ≤ H) (g : Frame P H 1 → ℝ) :
    ∃ m : ℝ, 𝔼 F, (g F - m) ^ 2 ≤ 36864 * H ^ 2 *
      ∑ p : {p : Fin H × Fin H // p.1 ≠ p.2}, 𝔼 F, (g (Frame.mapSL (SpecialLinearGroup.transvection p.2 1) F) - g F) ^ 2

def affineGenerator H : {p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H → SpecialLinearGroup (Fin H) ℤ × (Fin H → ℤ)
  -- inl (a, b) ↦ (1 + E_ab, 0),  inr i ↦ (1, e_i)
def affineMove P H L r k : Equiv.Perm (Frame P H r × (Fin H → ZMod L)) :=
  coordMove (affineGenerator H k).1 (affineGenerator H k).2
theorem card_affineGenerator_index : Fintype.card ({p : Fin H × Fin H // p.1 ≠ p.2} ⊕ Fin H) = H ^ 2

theorem expect_sq_le_affineMove [Fact P.Prime] [NeZero L] (hH : 3 ≤ H)
    (f : Frame P H 1 × (Fin H → ZMod L) → ℝ) (hf : 𝔼 p, f p = 0) :
    𝔼 p, f p ^ 2 ≤ 38912 * H ^ 2 * ∑ k, 𝔼 p, (f (affineMove P H L 1 k p) - f p) ^ 2
theorem secondEigenvalue_ofPerms_affineMove_le [Fact P.Prime] [NeZero L] (hH : 3 ≤ H) :
    (ofPerms (affineMove P H L 1)).secondEigenvalue ≤ 1 - 1 / (77824 * H ^ 4)
theorem spectralExpansion_lazy_ofPerms_affineMove_le [Fact P.Prime] [NeZero L] (hH : 3 ≤ H) :
    (ofPerms (affineMove P H L 1)).lazy.spectralExpansion ≤ 1 - 1 / (155648 * H ^ 4)
theorem expect_walk_pow_sliceGraph_affineMove_sub_expect_sq_le [Fact P.Prime] [NeZero L]
    (hH : 3 ≤ H) (hL : L ≤ P) (y : ZMod P) (f : RetentionSlice P H 1 L y → ℝ) (t : ℕ) :
    𝔼 A, (((sliceGraph L hL y (ofPerms (affineMove P H L 1)).lazy).walk ^ t) f A - 𝔼 B, f B) ^ 2 ≤
      (1 - 1 / (155648 * H ^ 4)) ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 2

The last theorem is #1691's expect_walk_pow_sliceGraph_sub_expect_sq_le with G the lazy affine walk and hG discharged. The constant depends only on H. The moves are #1691's coordMove by definition, so walk_sliceGraph_ofPerms_eq (the validated variants) applies to affineGenerator, for the non-lazy walk.

Proof. For f of mean zero, write g F = 𝔼 w, f (F, w). Then 𝔼 f² = 𝔼 g² + 𝔼 (f − g)².

• Box part (step 1). Apply feat(Expander): Efron–Stein and the coordinate-pair bound for shears and translations #1699's expect_sq_sub_expect_le_pairShearTranslation with Y = Frame P H 1, ρ i j the action of 1 + E_ij on frames, and partners σ i ≠ i. Each of its pair moves is an affine move, so 𝔼 (f − g)² ≤ 512 · 4H · Dir(f).
• Frame part (step 2). Frame.equivNeZero turns feat(Expander): Poincaré inequality for elementary moves on the nonzero vectors of (ZMod P)^H #1703's masked averages over (ZMod P)^H into averages over frames. The zero vector is fixed by the moves, so both sides scale by |Frame| / P^H, which cancels. This gives exists_expect_sq_sub_le_mapSL_transvection, applied to g. Since 𝔼 g = 0, 𝔼 g² ≤ 𝔼 (g − m)². By Jensen's inequality, the change of g along 1 + E_ab is at most that of f along the affine move, because the move acts on w by a bijection.
• Moves (step 3). affineMove_inl and affineMove_inr identify the moves pointwise: (F, w) ↦ ((1 + E_ab) F, w + w_b e_a) and (F, w) ↦ (F, w + e_i). The general input is transvection_mulVec.
• Gap (step 4). Combining gives 38912 H². Then secondEigenvalue_ofPerms_le with |K| = H² (card_affineGenerator_index), and the lazy bound spectralExpansion_lazy_le_one_add_secondEigenvalue_div_two.

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

Preprint	Lean
Lemma 6.1, p. 30: "Let S consist of the elementary matrices with a single ±1 off the diagonal, acting linearly, and the translations by ±e_i"	affineGenerator (forward generators; the inverses come from ofPerms), affineMove
Lemma 6.1, p. 30: the lazy operator K_H = I/2 + (1/(2m)) ∑_{g∈S} ρ(g) has a spectral gap depending only on H (via Shalom's property (T))	expect_sq_le_affineMove, secondEigenvalue_ofPerms_affineMove_le, spectralExpansion_lazy_ofPerms_affineMove_le: only for the action on Frame P H 1 × (ℤ/L)^H, gap 1/(155648 H⁴), proved elementarily
Proof of Lemma 6.2, p. 31: coordinates (F, w), action (F, w) ↦ (MF, Mw + c) mod P and mod L; "This action is transitive"	affineMove is #1691's coordMove; transitivity is not stated separately, it follows from the gap (test client)
Lemma 6.2, p. 31: ‖K^d − Π‖ decays on the conditional space with constants "independent of the field size, retention side lengths, … indicated identifiers"	expect_walk_pow_sliceGraph_affineMove_sub_expect_sq_le (L², one channel, r = 1)

Credit. The paper's text derives Lemma 6.1 from Shalom's property (T). The elementary route follows OpenAI's Lean development: lean/OAI/Computability/Logspace/AffineSampling.lean at rev 7ef5c0cc, declarations ExactDerandomization.Analysis.Square.square_gap, slice_frame, frame_gap and slice_gap. That is, it goes from the two-dimensional gap through coordinate pairs to frames, then assembles the slice gap. The module docstring names these declarations. Our statements and proofs are independent. I did not read that code; the declaration names come from the coordinator.

Differences from the source.

• Frames of length one only (h₀ = 2, r = 1), as in feat(Expander): Poincaré inequality for elementary moves on the nonzero vectors of (ZMod P)^H #1703.
• H ≥ 3, as in Lemma 6.1; the paper's H ≥ 4 satisfies it.
• One channel, L² only.
• The statements are ours.

Tests (ComplexityTests/SliceGap.lean, 93 lines):

• a transvection on an integer vector;
• three concrete affine moves on Frame 5 3 1 × (ZMod 4)^3, with wrap-around modulo 5 on the frame and modulo 4 on the box coordinate;
• the counts |Frame 5 3 1| = 124 and 9 generators for H = 3;
• conditional averaging on every retention slice of 𝔽₅^3 with side 3, every hypothesis discharged: decay (1 − 1/12607488)^(2t);
• a client deriving transitivity: for every prime P and every L, a function on Frame P 3 1 × (ZMod L)^3 invariant under the affine moves is constant;
• step 5 with feat(Expander): spectral gap of box products of permutation multigraphs #1693: for all primes P, P' and sides L, L', the lazy box product of the affine walks of two channels has spectral expansion at most 1 − 1/25214976.

Validation at bc81c6ab3: scripts/check.sh (all six gates), 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.

Catalogue assessment: no selected abstract, bridge, endpoint statement or renderer changes.

Remaining for Phase 3 (#1682):

• the J-component product (channels plus the free-bit torus (ℤ/2^q)^H with its own affine action), giving gap γ/J. feat(Expander): spectral gap of box products of permutation multigraphs #1693 gives the binary step, and the test shows two channels. The free-bit component needs the box-only Poincaré inequality, which is feat(Expander): Efron–Stein and the coordinate-pair bound for shears and translations #1699 with a trivial spectator. Then iterate.
• frames of length r ≥ 2 (the paper allows 2 ≤ h₀ < H). These need a different fibration, as noted on feat(Expander): Poincaré inequality for elementary moves on the nonzero vectors of (ZMod P)^H #1703.
• multi-step validated words and the L⁴/L^s form on slices (feat(Expander): fourth-moment decay of the random walk from the spectral gap #1685 with feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691);
• the frame-conditioned rank-channel estimates (Lemma 3.1, items 2–4).

Review: please arrange a non-author review of correctness, the API (the names affineGenerator/affineMove, Frame.equivNeZero, the placement of the transvection lemmas in Foundations/LinearAlgebra/Matrix) and the source mapping. Only commit bc81c6ab3 is new here.

Integration refresh (2026-10-30): merged the refreshed parents #1691 ae99b483b, #1703 efd5aa27b and #1693 3860f88e0 (each contains origin/main 311e984) at 8804d42c4, no rebase; merging #1691 first avoids the RetentionChannel.lean add/add conflict, after which all merges were clean. Own-layer diff against the merged parents is 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 8804d42c4.

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

🤖 Generated with Claude Code

[chris-ai1]

reviewer-crei-opus (agent review, not human approval; advisory: same session as the authoring workers). Head bc81c6ab33076a50ac4b0c25f39fc26888ae39ee, own commit bc81c6ab3 only. It sits on the merges of #1703 0e293465b, #1691 53de6a3f6 and #1693 a9e19a53a, which have their own reviews. Verdict: FINAL. No blocking findings.

Constant chain.

• Masked to Frame. expect_ite_eq shows that the masked average over (ZMod P)^H is exactly c·𝔼_Frame, with c = |Frame|/P^H. In exists_expect_sq_sub_le_mapSL_transvection both sides pick up the same c: the left side by expect_ite_eq, the right side because the moves fix 0 (h0). So c cancels via le_of_mul_le_mul_left, with no loss of a factor 2, and feat(Expander): Poincaré inequality for elementary moves on the nonzero vectors of (ZMod P)^H #1703's 36864 H² carries over unchanged.
  • Frame.equivNeZero (linearIndependent_unique_iff) and Frame.card_one = P^H − 1 are correct.
  • mapSL_transvection_apply_zero identifies 1 + E_ab on frames with elementaryMove a b.
• Box part. feat(Expander): Efron–Stein and the coordinate-pair bound for shears and translations #1699's pair bound with Y = Frame P H 1 (a Type, as feat(Expander): Efron–Stein and the coordinate-pair bound for shears and translations #1699 requires), ρ i j = mapSL (transvection (i≠j) 1) and partner σ i ≠ i. All four pair moves are literally affine moves: inl (i,σi), inl (σi,i), inr i, inr σi, verified by simp in hpair. That gives 512·4·H·D = 2048 H·D.
• Frame part. g F = 𝔼_w f(F,w) has mean 0, so 𝔼g² ≤ 𝔼(g−m)². Jensen (sq_expect_sub_expect_le) applies because affineMove (inl p) is prodCongr of a frame permutation and a bijection of w, and only the inl moves are used, so the frame Dirichlet form is ≤ D.
• Total. 2048 H + 36864 H² ≤ 38912 H² for H ≥ 1. ✓
• Spectral bounds. secondEigenvalue_ofPerms_le with c = 1/(38912 H²) and |K| = H² (card_affineGenerator_index: H(H−1)+H) gives 1 − 1/(77824 H⁴). The lazy walk halves the gap, giving 1/(155648 H⁴). In the test, 155648·81 = 12607488 ✓.

Moves equal coordMove. affineMove is defined as coordMove (affineGenerator k).1 (affineGenerator k).2, so #1691's lemmas apply directly. affineMove_inl/_inr give the explicit pointwise forms ((1+E_ab)F, w + w_b e_a) and (F, w + e_i) via transvection_mulVec.

hL : L ≤ P. It is only passed through to #1691's sliceGraph/expect_walk_pow_sliceGraph_sub_expect_sq_le, where the retention side must fit inside ZMod P. That is appropriate, and the gap itself (expect_sq_le_affineMove, the eigenvalue bounds) needs only [NeZero L], uniform in P, L and y.

Mathlib reuse. It reuses Matrix.SpecialLinearGroup.transvection and transvection_coe. Mathlib (local copy) has only transvection_mulVec_single_self/_other and nothing for general vectors or ring maps, so transvection_mulVec and map_transvection are not duplicates. They are good upstream candidates. Nit: they are global @[simp] lemmas in a Mathlib namespace, so recheck for name clashes on the next Mathlib bump.

Tests. I checked the following by hand:

• the transvection example: 1 + 2·(−3) = −5;
• the frame move (1,0,4) ↦ (0,0,4), using 1+4 ≡ 0 mod 5;
• the box move 3+2 ≡ 1 mod 4, and the translation 3+1 ≡ 0 mod 4;
• the counts 124 and 9.

Beyond those:

• The conditional-averaging instance has all hypotheses discharged.
• The transitivity client is nonvacuous: invariance under the moves makes f constant, for every prime P and every L.
• The two-channel box product reaches 1 − 1/25214976 via feat(Expander): spectral gap of box products of permutation multigraphs #1693.

Credit and provenance. The docstring cites preprint Lemmas 6.1/6.2. It names AffineSampling.lean @ 7ef5c0cc (Square.square_gap, slice_frame, frame_gap, slice_gap) with "not consulted". It states the limits: r = 1, one channel, L².

Nit: a stray double blank line before nontrivial_frame_one.

Limits: I ran no Lean build, so I rely on the PR's check.sh and hosted CI. I did not re-review #1691, #1693, #1699 or #1703. The Mathlib duplicate check used the local Mathlib checkout, not necessarily the exact rc2 pin.

[edemaine]

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

Reviewed the complete own layer and clean parent merges, reusing the current-head coverage of #1703, #1691 and #1693. No blocking findings. The masked-to-frame normalization cancels on both sides; the box/frame variance decomposition and Jensen step give 38912 H². With H² forward generators, inverse symmetrization and laziness give gap 1/(155648 H⁴). The transvection lemmas reuse Mathlib's matrices and belong in the general matrix module.

Checked the mapping to pinned preprint Lemmas 6.1–6.2 (pp. 30–31) and the credited AffineSampling declarations. This establishes the stated one-channel, length-one-frame L² result for prime P, H ≥ 3 and positive L (L ≤ P for retention slices), uniformly in the moduli and identifier; it does not establish the remaining higher-frame or higher-moment endpoints. The concrete modular moves, counts and fully discharged F₅ conditional-averaging test are nonvacuous. No curated-abstract impact.

Hosted Lean CI and title checks passed at this SHA. I ran no local Lean build. Live head rechecked before posting.

[edemaine]

reviewer-codex-edemaine: APPROVE at 8804d42c442bb9be2643913f5b1c213dbca27fbc (independent agent integration-delta review, not human approval). Reuse my whole-layer correctness/API/source review and the refreshed #1703/#1691/#1693 parent reviews.

Transvection, SliceGap and the concrete tests are byte-identical to approved bc81c6ab3. Full-tree comparison confirms exactly the reviewed parent union plus those three files and their two aggregate imports; no unexpected blob/mode changes. The rank-one-frame L² hypotheses, gap normalization and source/model scope remain unchanged; no curated-abstract impact.

git diff --check passes. Exact-head Lean CI 41036098128 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]

Non-author coordinator Codex roadmap_learning published the audited normal restack at 3537ac9771e4f0ba213b491c64a5329bffb21ace, using an ordinary fast-forward after fresh ownership and head guards. Independent preservation audit confirmed all three original source/test modes and blobs, the complete original bc81c6ab3 nonaggregate patch, all nine direct/side-parent files and every unrelated main entry. Only generated imports were resolved; the checkpoint has 3,151 canonical imports.

Fresh required PR CI passed all six gates. Actual checkout 0782bf13 merges source 3537ac97 into accepted main b48b310f; its complete tree 6bcc9151 equals the audited checkpoint, with the original feature patch, reviewed payloads, pins and every unrelated main entry exact. Under the validated coordinator-fix rule, APPROVE 3537ac9 for this generated-import restack (agent review, not human approval). The outside mathematics/API/source review is reused for the unchanged feature and credit. Abstract assessment: no statement, definition, proof, model/resource scope, catalogue or renderer change in the restack.

Scope remains one channel, frames of length one, an L² bound, prime P, H ≥ 3 and positive L, with L ≤ P on retention slices. General frames, higher moments and full estimator/native realization remain outside this result; #1682/#1444/#474 stay open. #1706’s parent has landed; its existing external integration owner retains that follow-up.

Required MQ 41159951433 passed all six gates. This PR actually landed at b0e7dcf8 on 2026-10-31 at 02:40:27 UTC. Its sole parent and expected tree match the independently checked physical candidate; the complete original three-file feature patch and reviewed modes/blobs remain exact on actual main. The fixed covering main consumer at 238913b4 is terminal SUCCESS with all six gates. It restored exact-head MQ 41160134172, attempt 1, without rebuilding library/test modules and published at 02:59:00.7323151 UTC.

Public-cache closeout: the published map has 4,249 unique entries (191,218 bytes; SHA-256 b6887ad262da9aeb553f9927e851c9305b7459d89a4ba374f87abea0204964b6). All 27 new artifact references versus the verified saved #1862 baseline return HEAD 200 with positive lengths; unchanged references reuse that verified chain. One finalized log and map GET, zero artifact bodies or repeated baseline GETs. Source, queue, actual landing and usable-cache follow-through are complete.