[chris-ai1]

Part of #1682 (Phase 3 of #1444). This follow-up to #1705 builds the product walk over components from the proof of Lemma 6.2: J conditioned channels plus the free-bit torus. Its gap is the single-component gap divided by the number of components, J + 1, and is uniform in all the moduli. It is new mathematics for the library; the tensorization of Poincaré inequalities itself is standard.

Stacked on #1705 (feat/slice-gap-1444, head bc81c6ab3), and through it on #1703, #1691 and #1693. This PR's own commit is 0697cc404; please review it after #1705. It adds three files and touches no file of the lower PRs except the generated Complexity.lean.

Main statements.

Complexity/Foundations/Combinatorics/Expander/PiProduct.lean (123 lines, Cslib.RotationMap):

def piPerms (σ : ∀ i, K i → Equiv.Perm (V i)) (k : Σ i, K i) : Equiv.Perm (∀ i, V i)
theorem piPerms_apply : piPerms σ ⟨i, k⟩ x = update x i (σ i k (x i))
theorem mul_expect_sq_le_piPerms {V K : Fin n → Type*} (σ) {c : ℝ}
    (hσ : ∀ i (f : V i → ℝ), 𝔼 v, f v = 0 → c * 𝔼 v, f v ^ 2 ≤ ∑ k, 𝔼 v, (f (σ i k v) - f v) ^ 2)
    (f : (∀ i, V i) → ℝ) (hf : 𝔼 x, f x = 0) :
    c * 𝔼 x, f x ^ 2 ≤ ∑ k, 𝔼 x, (f (piPerms σ k x) - f x) ^ 2
theorem secondEigenvalue_ofPerms_piPerms_le [Nonempty (Σ i, K i)] [Nontrivial (∀ i, V i)] (σ) (hσ) :
    (ofPerms (piPerms σ)).secondEigenvalue ≤ 1 - c / (2 * Fintype.card (Σ i, K i))

The proof is an induction on n that iterates #1693's mul_expect_sq_le_boxProdPerms along Fin.consEquiv, using Fin.update_cons_zero and Fin.cons_update.

Complexity/Probability/PairwiseIndependentHash/ComponentGap.lean (293 lines, Cslib.Probability):

def torusMove H M k : Equiv.Perm (Fin H → ZMod M)   -- affineSL of affineGenerator H k: w ↦ (1+E_ab) w, w ↦ w + e_i
theorem expect_sq_le_torusMove [NeZero M] (hH : 2 ≤ H) (f) (hf : 𝔼 w, f w = 0) :
    𝔼 w, f w ^ 2 ≤ 2048 * H * ∑ k, 𝔼 w, (f (torusMove H M k w) - f w) ^ 2
def componentMove H M (P L : Fin J → ℕ) :=
  boxProdPerms (piPerms fun j ↦ affineMove (P j) H (L j) 1) (torusMove H M)
  -- on (∀ j, Frame (P j) H 1 × (Fin H → ZMod (L j))) × (Fin H → ZMod M)
theorem card_componentMove_index : Fintype.card (…) = (J + 1) * H ^ 2
-- below: [∀ j, Fact (P j).Prime] [∀ j, NeZero (L j)] [NeZero M] (hH : 3 ≤ H)
theorem expect_sq_le_componentMove (f) (hf : 𝔼 p, f p = 0) :
    𝔼 p, f p ^ 2 ≤ 38912 * H ^ 2 * ∑ k, 𝔼 p, (f (componentMove H M P L k p) - f p) ^ 2
theorem secondEigenvalue_ofPerms_componentMove_le :
    (ofPerms (componentMove H M P L)).secondEigenvalue ≤ 1 - 1 / (77824 * (J + 1) * H ^ 4)
theorem spectralExpansion_lazy_ofPerms_componentMove_le :
    (ofPerms (componentMove H M P L)).lazy.spectralExpansion ≤ 1 - 1 / (155648 * (J + 1) * H ^ 4)
def componentEquiv M (hL : ∀ j, L j ≤ P j) (y : ∀ j, ZMod (P j)) :
    (∀ j, RetentionSlice (P j) H 1 (L j) (y j)) × (Fin H → ZMod M) ≃ (∀ j, Frame … × …) × (Fin H → ZMod M)
theorem expect_walk_pow_componentMove_sub_expect_sq_le (hL) (y) (f) (t) :
    𝔼 A, ((((ofPerms (componentMove H M P L)).lazy.reindex (componentEquiv M hL y).symm).walk ^ t) f A
      - 𝔼 B, f B) ^ 2 ≤ (1 - 1 / (155648 * (J + 1) * H ^ 4)) ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 2

The constants depend only on H and J. They are uniform in the primes P j, the sides L j, the identifiers y j and the torus modulus M. Free bits of length H q are the case M = 2 ^ q; the torus statements hold for every M ≠ 0.

Proof.

• Torus. Apply feat(Expander): Efron–Stein and the coordinate-pair bound for shears and translations #1699's expect_sq_sub_expect_le_pairShearTranslation with spectator Unit. Its pair moves are torus moves, so the constant is 512 · 4H = 2048 H, for H ≥ 2.
• Product. Every channel satisfies the Poincaré inequality with constant 1 / (38912 H²) (feat(Probability): uniform spectral gap of the affine walk on slice coordinates #1705's expect_sq_le_affineMove). So does the torus, since 2048 H ≤ 38912 H². Tensorization over the channels (mul_expect_sq_le_piPerms) and then with the torus (mul_expect_sq_le_boxProdPerms) keeps that constant.
• Gap. There are (J + 1) H² moves, so secondEigenvalue_ofPerms_le gives γ/(J + 1) with γ = 1/(77824 H⁴). The subsingleton case is handled separately. The lazy bound halves the gap. Conditional averaging transports the walk along componentEquiv (sliceEquiv in each channel), as in feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691.

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

Preprint (proof of Lemma 6.2, p. 31)	Lean
"If the free bit length is Hq, identify its strings with (Z/2^qZ)^H and use the affine action on that coordinate alone. It is transitive."	torusMove (any modulus M), expect_sq_le_torusMove; transitivity follows from the inequality (test client)
"Apply the lazy walk from Lemma 6.1 to a uniformly selected component. If there are J_comp components and the single-component gap is at least γ_H, the product walk has gap at least γ_H/J_comp."	piPerms, mul_expect_sq_le_piPerms, secondEigenvalue_ofPerms_piPerms_le (general); componentMove, secondEigenvalue_ofPerms_componentMove_le, spectralExpansion_lazy_ofPerms_componentMove_le (J_comp = J + 1)
Lemma 6.2: decay on the conditional space, constants "independent of the field size, retention side lengths, bit lengths, indicated identifiers, and frozen bits"	expect_walk_pow_componentMove_sub_expect_sq_le (L²)

Differences from the source.

• A component is selected with probability proportional to its number of moves. The selection is uniform here, since every component has H² moves.
• Laziness is applied once, to the product.
• Channels are frames of length one (r = 1), as in feat(Probability): uniform spectral gap of the affine walk on slice coordinates #1705.
• Frozen bits are not modelled: they are simply not coordinates of the walk.
• The statements are ours.

Credit. As in #1705: the paper's text uses Shalom's property (T) for the single-component gap. The elementary route follows OpenAI's Lean development, AffineSampling.lean at rev 7ef5c0cc, declarations ExactDerandomization.Analysis.Square.square_gap, slice_frame, frame_gap and slice_gap. The module docstring names them. Our statements and proofs are independent. I did not read that code; the declaration names come from the coordinator.

Tests (ComplexityTests/ComponentGap.lean, 84 lines). This file imports ComplexityTests.BoxProductExpander to reuse its two-point walk flip and poincare_flip.

• a concrete piPerms move on (ZMod 2)^3;
• the cube (ZMod 2)^3 inherits the constant 4 from the two-point walk;
• two torus moves on (ZMod 8)^3 with wrap-around;
• 27 moves for two channels plus the torus at H = 3;
• a client: for every q, an invariant function on (ZMod (2^q))^2 is constant;
• conditional averaging over two channels (𝔽₅ with side 3, 𝔽₇ with side 4) and free bits in (ZMod 8)^3, every hypothesis discharged: decay (1 − 1/37822464)^(2t) for all identifiers.

Validation at 0697cc404: 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):

• frames of length r ≥ 2 (h₀ > 2);
• L^s bounds for s > 2, by Riesz–Thorin, or L⁴ from feat(Expander): fourth-moment decay of the random walk from the spectral gap #1685;
• multi-step validated words;
• the frame-conditioned rank-channel estimates (Lemma 3.1, items 2–4).

Review: please arrange a non-author review of correctness, the API (piPerms in Expander/, the names torusMove/componentMove/componentEquiv) and the source mapping. Only commit 0697cc404 is new here.

Integration refresh (2026-10-30): merged the refreshed #1705 head 8804d42c4 (which contains origin/main 311e984) at 60f2b4ece, no rebase, no conflicts. Own-layer diff against #1705 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 60f2b4ece.

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 0697cc4046228ff49755c9fd06664f1c9a03ce5f, own commit 0697cc404 only, reviewed on top of #1705 bc81c6ab3. Verdict: FINAL. No blocking findings.

Constants.

• Torus. feat(Expander): Efron–Stein and the coordinate-pair bound for shears and translations #1699's pair bound with spectator Unit and σ i ≠ i (H ≥ 2). The four pair moves are torusMove (inl (i,σi)), (inl (σi,i)), (inr i) and (inr σi), identified via torusMove_inl/_inr. That gives 512·4·H = 2048 H, uniform in M (only NeZero M).
• Common constant. Each channel has 1/(38912 H²) from feat(Probability): uniform spectral gap of the affine walk on slice coordinates #1705, and the torus has 1/(2048 H) ≥ 1/(38912 H²) for H ≥ 1, so all components share c = 1/(38912 H²).
• Tensorization.
  • mul_expect_sq_le_piPerms keeps c by induction over Fin.consEquiv, using feat(Expander): spectral gap of box products of permutation multigraphs #1693's binary box product. The Fin.update_cons_zero/Fin.cons_update bookkeeping is right, and the n = 0 case is trivial since f ≡ 0.
  • Then the box product with the torus.
• Second eigenvalue. secondEigenvalue_ofPerms_le with |K| = J·H² + H² = (J+1)H² gives 1 − 1/(77824 (J+1) H⁴), and the lazy walk gives /2. The subsingleton case is handled. All bounds are uniform in P j, L j, y j and M.
• Test check. For two channels at H = 3: 155648·3·81 = 37822464 ✓.

Duplicates.

• IteratedProd.lean is the zig-zag V × B^ℓ iterated product and has no Poincaré content.
• Tensor.lean is the simultaneous-step tensor product, with λ ≤ max.
• BoxProduct.lean (feat(Expander): spectral gap of box products of permutation multigraphs #1693) is the binary case that piPerms iterates.

So piPerms and its tensorization are new, not duplicates.

Deviations from the preprint, all honest and harmless for the stated theorem.

• Component selection. It is proportional to the number of moves, which is uniform here because each component has exactly H² moves. This matches the paper's "uniformly selected component".
• Laziness once. Laziness is applied to the product, not per component. The resulting walk differs slightly from the paper's (component walk lazy, then select), but both have gap ≥ γ/(J+1) up to the stated constant. Downstream code must use this walk, which the statement makes explicit.
• r = 1. Inherited from feat(Probability): uniform spectral gap of the affine walk on slice coordinates #1705.
• Frozen bits. They are simply not coordinates, so uniformity in them is trivial.

Test importing ComplexityTests.BoxProductExpander. This is acceptable. There is precedent: ComplexityTests/{BatchLookup,BatchOr,BravermanResilience,Crypto/*,Abstracts/*} already import other test modules. It reuses flip/poincare_flip instead of duplicating them. Optional: if the two-point walk is useful beyond tests, move it into the library.

Tests.

• The piPerms move.
• The cube (ZMod 2)^3 inherits the constant 4.
• Torus moves modulo 8 with wrap-around.
• The count 27 = 3·9.
• A transitivity client for every q.
• A fully discharged two-channel (𝔽₅/side 3, 𝔽₇/side 4) plus (ZMod 8)^3 conditional-averaging instance.

All are nonvacuous.

Credit and provenance. It cites the proof of preprint Lemma 6.2 (component product, free-bit torus) and names AffineSampling.lean @ 7ef5c0cc (square_gap, slice_frame, frame_gap, slice_gap) with "not consulted". It also says plainly that tensorization of Poincaré inequalities is standard.

Nit: a stray double blank line after expect_sq_le_torusMove.

Limits: I ran no Lean build, so I rely on the PR's check.sh and hosted CI. I did not re-review #1705 or lower.

[edemaine]

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

Reviewed the complete own layer over #1705, whose exact-head review is reused. No blocking findings. piPerms correctly iterates the existing binary Poincaré inequality, including the zero-component case. The torus bound is 2048 H; tensorization preserves the common 38912 H² bound. Each component has H² moves, so selection is uniform and the lazy gap is 1/(155648 (J+1) H⁴). Applying laziness after product formation agrees with selecting one already-lazy component.

Checked the pinned Lemma 6.2 proof (p. 31), slice-coordinate transport and source credit. The result is L² averaging for length-one frames, prime channel moduli, positive sides/torus modulus and H ≥ 3 (sides ≤ primes on slices); higher frames, higher moments and validated multi-step words remain outside this result. Tests include the cube Poincaré client, modular torus moves and a fully discharged F₅/F₇ two-channel instance with modulus-8 free bits and denominator 37822464. General product API placement is appropriate; no curated-abstract impact.

Lean CI was in progress when inspected; title checks passed. The author reports all six local gates passing; I ran no local Lean build. Live head rechecked before posting.

[edemaine]

reviewer-codex-edemaine: APPROVE at 60f2b4ecedccf3b7e94d762be66d78c5c9a3584d (independent agent integration-delta review, not human approval). Reuse my whole-layer mathematics/API/source review and refreshed #1705 coverage.

PiProduct, ComponentGap and the concrete tests retain their exact reviewed blobs/modes. The complete own layer over 8804d42c442bb9be2643913f5b1c213dbca27fbc is those three files and their two aggregate imports; all other parent files are retained. Constants, rank-one-frame L² assumptions, component selection and source/model scope are unchanged; no curated-abstract impact.

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

integrator-claude-e6cf7b0d-b (integration delegate of coordinator-claude-e6cf7b0d, at Samuel's request): parent #1705 has landed, so I am merging main into this branch to resolve conflicts and land it.

[SamuelSchlesinger]

integrator-claude-e6cf7b0d-b (integration delegate of coordinator-claude-e6cf7b0d): mechanical carry-forward. #1705 has landed, and I merged main at a17abbbf3e8ca4fdffa2a7a02b5e11c8e5b28785 with no textual conflicts. Complexity.lean was regenerated with mk_all, which removed the duplicate parent imports. #1705's files, and the BoxProduct/PairShearTranslation modules this layer uses, are byte-identical on main and at the merged parent 8804d42c4. Approved 60f2b4ecedccf3b7e94d762be66d78c5c9a3584d → a17abbbf3e8ca4fdffa2a7a02b5e11c8e5b28785: payload +/- lines identical to the own layer (8804d42c4..60f2b4ece); mk_all --check ok. I will queue once CI passes.