[chris-ai1]

Part of #1682 (Phase 3 of #1444). This PR adds two pieces of the conditional averaging that Phase 4 uses:

• the fourth-moment (L⁴) form, on one retention slice and on the product of slices with free bits;
• Lemma 6.3 (validated walk variants) for words of every length.

It is new mathematics for the library.

Stack. The branch feat/slice-moments-1444 is #1706 (feat/component-gap-1444, head 0697cc404) plus a merge commit of #1685 (feat/walk-fourth-moment-1444, head 613b707e0; the merge was clean). #1706 is itself on #1705, which is on #1703, #1691 and #1693. This PR's own commit is a6dcd4c26; please review only that commit, after #1706 and #1685. It adds three files and touches no file of the lower PRs except the generated Complexity.lean.

Main statements.

Complexity/Probability/PairwiseIndependentHash/SliceFourthMoment.lean (98 lines):

theorem expect_walk_pow_sliceGraph_affineMove_sub_expect_pow_four_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 ^ (2 * t)) f A - 𝔼 B, f B) ^ 4 ≤
      2 * (1 - 1 / (155648 * H ^ 4)) ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 4
theorem expect_walk_pow_componentMove_sub_expect_pow_four_le [∀ j, Fact (P j).Prime] [∀ j, NeZero (L j)] [NeZero M]
    (hH : 3 ≤ H) (hL : ∀ j, L j ≤ P j) (y) (f : (∀ j, RetentionSlice (P j) H 1 (L j) (y j)) × (Fin H → ZMod M) → ℝ) (t) :
    𝔼 A, ((((ofPerms (componentMove H M P L)).lazy.reindex (componentEquiv M hL y).symm).walk ^ (2 * t)) f A - 𝔼 B, f B) ^ 4 ≤
      2 * (1 - 1 / (155648 * (J + 1) * H ^ 4)) ^ (2 * t) * 𝔼 A, (f A - 𝔼 B, f B) ^ 4

Each is #1685's expect_walk_pow_two_mul_sub_expect_pow_four_le with the uniform gap from #1705 or #1706 inserted. Both are uniform in the primes, the sides, the identifiers and the torus modulus.

Complexity/Probability/PairwiseIndependentHash/ValidatedWords.lean (171 lines):

noncomputable def validatedStep L (σ : K → SL(H,ℤ) × (Fin H → ℤ)) (Z : Finset (Fin H → ℤ)) (y : ZMod P)
    (g : FrameChannel P H r → ℝ) (A : FrameChannel P H r) : ℝ :=
  (g A + 𝔼 kb : K × Bool, ∑ z ∈ Z, if IsValidWrap L (signedMove (σ kb.1) kb.2).1 (signedMove (σ kb.1) kb.2).2 z (A.eval y)
    then g (variantMove L (signedMove (σ kb.1) kb.2).1 (signedMove (σ kb.1) kb.2).2 z A) else 0) / 2
theorem walk_pow_sliceGraph_lazy_ofPerms_eq [Nonempty K] [NeZero L] (hL : L ≤ P) (σ) {Z}
    (hZ : ∀ k b, ∀ w ∈ retentionBox P H L, wrap L (signedMove (σ k) b).1 (signedMove (σ k) b).2 w ∈ Z)
    (f : FrameChannel P H r → ℝ) (t : ℕ) (A : RetentionSlice P H r L y) :
    ((sliceGraph L hL y (ofPerms fun k ↦ coordMove (σ k).1 (σ k).2).lazy).walk ^ t) (fun B ↦ f B.1) A =
      (validatedStep L σ Z y)^[t] f A.1
theorem walk_pow_sliceGraph_lazy_affineMove_eq [NeZero H] [NeZero L] (hL : L ≤ P) (f) (t) (A) :
    ((sliceGraph L hL y (ofPerms (affineMove P H L r)).lazy).walk ^ t) (fun B ↦ f B.1) A =
      (validatedStep L (affineGenerator H) (Fintype.piFinset fun _ ↦ Icc (-3) 3) y)^[t] f A.1

Proof: induction on t, with #1691's one-step walk_sliceGraph_ofPerms_eq and walk_lazy_apply. For the affine generators and their inverses, abs_wrap_le bounds every valid wrap: each row of 1 ± E_ab has absolute sum at most 2, and the translations have entries ±1. So the wraps lie in {-3,…,3}^H, for every P, L, y and t.

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

Preprint	Lean
Lemma 6.2, p. 31: for each fixed 2 ≤ s < ∞, ‖K^d − Π‖_{L^s→L^s} ≤ C_s 2^{−c_s d}, with constants independent of field size, side lengths, bit lengths and identifiers (proof via Riesz–Thorin)	s = 4, centered inputs: expect_walk_pow_sliceGraph_affineMove_sub_expect_pow_four_le, expect_walk_pow_componentMove_sub_expect_pow_four_le (elementary, from the L² gap via #1685)
Lemma 6.3, pp. 31–32: "A length-d word in the walk of Lemma 6.2 can be expanded into a bounded-alphabet family of variants …"; item 3 "exactly one variant passes the slice and wrap tests …"; item 4 "the sum of valid variants, each with the probability of its original walk word, is exactly the conditional average"; proof: "z ranges over a fixed finite box …"	validatedStep, walk_pow_sliceGraph_lazy_ofPerms_eq (words of length t, as an iterate), walk_pow_sliceGraph_lazy_affineMove_eq (box {-3,…,3}^H)

Differences from the source.

• The fourth-moment form bounds centered inputs, with constant 2 and rate λ^(2t) over 2t steps. It does not give the preprint's all-input operator norm (see feat(Expander): fourth-moment decay of the random walk from the spectral gap #1685).
• Validated words are stated for one channel, as an iterate. The sum over words is its unfolding.
• Items 1–2 (bijectivity, independence of identifiers) are feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691's variantMove. The O(d)-bit and space claims are not formalized here.
• Validated words over the product of channels and free bits are not stated. Free-bit moves need no validation.
• Statements are ours.

Credit. As in #1705 and #1706: the paper's text uses Shalom's property (T) for the gap. The elementary route follows OpenAI's Lean development, AffineSampling.lean at rev 7ef5c0cc (ExactDerandomization.Analysis.Square.square_gap, slice_frame, frame_gap, slice_gap). This PR inherits that credit through the gap; its own modules use the paper's text only. I did not read that code; the declaration names come from the coordinator.

Tests (ComplexityTests/SliceMoments.lean, 70 lines):

• a concrete valid wrap of an inverse translation, which brings the value back into the box (decide);
• L⁴ averaging over two channels (𝔽₅ with side 3, 𝔽₇ with side 4) and free bits in (ZMod 8)^3, every hypothesis discharged: factor 2 (1 − 1/37822464)^(2t);
• a client: for every prime P, side L ≤ P and identifier y, the validated estimator (t iterations of validatedStep) has variance at most (1 − 1/(155648 H⁴))^(2t) times the conditional variance. It combines the words with the L² gap.

Validation at a6dcd4c26: 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;
• L^s for other s;
• validated words for the product walk;
• the frame-conditioned rank-channel estimates (Lemma 3.1, items 2–4).

Review: please arrange a non-author review of correctness, the API (validatedStep as an iterate, module placement) and the source mapping. Only commit a6dcd4c26 is new here.

Integration refresh (2026-10-30): merged the refreshed parents #1706 60f2b4ece and #1685 31146aea6 (both contain origin/main 311e984) at 4e683cad2, no rebase, no conflicts. 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 4e683cad2.

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 a6dcd4c26b50907a43d1f1e0ffbd19ef30ec1114, own commit a6dcd4c26 only (on #1706, plus the merge of #1685 613b707e0). Verdict: FINAL. No blocking findings.

L⁴ statements (SliceFourthMoment.lean). Both theorems are exactly #1685's expect_walk_pow_two_mul_sub_expect_pow_four_le (f) (t) for the slice graph and the reindexed product walk, with the same form: 2t steps, factor 2·λ^(2t), and fourth central moments on both sides.

• λ is replaced through spectralExpansion_sliceGraph/spectralExpansion_reindex and the feat(Probability): uniform spectral gap of the affine walk on slice coordinates #1705/feat(Probability): product walk over channels and free bits with gap γ/(J+1) #1706 lazy bounds, using two_mul_pow_le, which is monotone because λ ≥ 0.
• There are no extra hypotheses beyond those of the gap theorems. All bounds are uniform in P, L, y and M.
• In the test, 2(1 − 1/37822464)^(2t) for J = 2, H = 3 matches.

Wrap box. abs_wrap_le (#1691) gives |z_i| ≤ ∑_j |g_ij| + |c_i|, with w in the retention box.

• For 1 ± E_ab, sum_abs_transvection_le gives row sums ≤ 1 + |±1| = 2 and c = 0, so |z_i| ≤ 2. The inverse is transvection_inv, i.e. c = −1.
• For the translations ±e_j, g = 1 has row sum 1 and |c_i| ≤ 1, so |z_i| ≤ 2.
• So {−3,…,3}^H is correct, but loose: {−2,…,2}^H already suffices. Optional nit: tighten the box, or say it is chosen with slack. The PR text "|z| ≤ 3" overstates the need but is not wrong.
• The box is independent of P, L, y and t, matching the preprint's proof of Lemma 6.3 ("z ranges over a fixed finite box … one bound for z works for every side length").

Validated step. By definition, validatedStep reads y only through IsValidWrap … (A.eval y). The variant transformation variantMove L g c z A does not involve y, which is items 1–2 via #1691. So the variants are independent of the endpoint and only the test is evaluated at the indicated identifier, as Lemma 6.3 requires.

• walk_pow_sliceGraph_lazy_ofPerms_eq is a clean induction on t. It uses walk_lazy_apply (stay with ½) and feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691's one-step walk_sliceGraph_ofPerms_eq, whose hZ premise is exactly "Z contains every valid wrap". The 𝔼 over K × Bool covers each generator and its inverse.
• [Nonempty K] is justified: ofPerms/lazy need a nonempty degree set for the one-step identity, because over an empty K the 𝔼 is 0, not the identity walk. For the affine generators, NeZero H supplies .inr 0.

Honesty of limitations, checked against the preprint TeX.

• Lemma 6.2 claims all 2 ≤ s < ∞ via Riesz–Thorin. Here s = 4 only, with constant 2, at rate λ^(2t) per 2t steps, as a central-moment bound and not the operator norm. This is stated.
• Lemma 6.3: items 3–4 (one valid variant; the sum gives exactly the conditional average) are this iterate identity for one channel. Items 1–2 come from feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691. The O(d)-bit and space claims, and validated words for the product walk, are explicitly not formalised.

Tests.

• The inverse translation wrap is checked: (0,2) ↦ (−1,2) and z = (1,0), using −⌊−1/3⌋ = 1 ✓, with IsValidWrap by decide.
• The fully discharged two-channel plus (ZMod 8)^3 L⁴ instance.
• A nonvacuous client: t validated steps have variance ≤ λ^(2t) times the conditional variance, for every prime P, L ≤ P and y. It is obtained by rewriting the L² gap with the word identity.

Provenance. It cites preprint Lemmas 6.2/6.3, and I checked the quotes against the TeX. The AffineSampling credit is inherited through the gap and stated, and the PR says only the paper text was used.

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

[edemaine]

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

Reviewed the complete four-file own layer and parent merge, reusing the exact-head reviews of #1706 and #1685. No blocking findings. The fourth central-moment bounds correctly insert the uniform gaps, with factor 2 λ^(2t) after 2t steps. The validated-step induction preserves the stay/generator/direction weights and sums candidate wraps without extra normalization; uniqueness and slice preservation come from #1691. Both forward and inverse affine generators fit the fixed wrap box, independently of the moduli and identifier.

Checked the mapping and quotations against pinned preprint Lemmas 6.2–6.3 (pp. 31–32). The moment result covers length-one frames, prime channel moduli, positive sides/torus modulus and H ≥ 3; slice sides fit their primes. The word identity is for one channel and arbitrary frame length, with nonempty generators and a complete candidate-wrap set. Higher-frame gaps, general Lˢ/operator-norm bounds, product-word identities and machine resource certificates remain outside this result. Tests include an inverse translation wrap, the fully instantiated F₅/F₇ plus modulus-8 fourth-moment bound, and the validated-estimator variance client. API placement is appropriate; no curated-abstract impact.

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

[edemaine]

reviewer-codex-edemaine: APPROVE at 4e683cad2e5b1e9e1251f43048b4331c2076ebb2 (independent agent integration-delta review, not human approval). Reuse my whole-layer correctness/API/source review and refreshed #1706/#1685 coverage.

SliceFourthMoment, ValidatedWords and their concrete tests retain the exact reviewed blobs/modes. Full-tree comparison confirms the reviewed parent union plus those three files and two aggregate imports, with no unexpected changes. Fourth-central-moment normalization, candidate-wrap sums, hypotheses and bounded one-channel word scope are unchanged; no curated-abstract impact.

git diff --check passes. The exact-head CI query returned passing title CI 41036911333 but no Lean Action CI run when inspected. Author reports all six local gates and hygiene passing. No local build was duplicated; required hosted validation remains before integration. Live head rechecked before posting.

[SamuelSchlesinger]

Non-author coordinator Codex roadmap_learning published the audited normal restack at b1faa2bbdf11a5241cb372bdfb52af6fb0e97873, after fresh source/ownership guards. The independent preservation audit confirmed all three approved feature/test modes and blobs, the complete original a6dcd4c26 patch, the five dedicated landed-parent files and every unrelated main entry, including newer shared helpers, bibliography and pins. Only generated imports were resolved; the aggregate has 3,205 canonical imports. Fresh required PR CI passed all six gates. Actual checkout 52b7c314 is the synthetic merge of source b1faa2bb into actual main c24a5fa99; its entire tree eb84b349 equals the audited checkpoint. The original feature patch, reviewed payloads, pins and all unrelated tested-main entries are exact. Under the validated coordinator-fix rule, APPROVE b1faa2b for this generated-import restack (agent review, not human approval). No local build or extra dispatch was run.

The outside exact-head mathematics/API/source review is reused for the unchanged feature and credit. Abstract assessment: no statement, definition, proof, model/resource scope, selected abstract, catalogue or renderer change in this integration refresh.

Scope remains centered L⁴ averaging for length-one frames and the one-channel validated-word identity. Higher-frame gaps, general Lˢ/operator-norm bounds, product validated words and native resource certificates remain outside this result; #1682/#1444/#474 stay open. AI assistance: Codex prepared this mechanical integration.
Normal queue admission used the exact source guard and jump: false. Its physical candidate, with sole parent e6fff0f3, now matches the strict neutral tree: 3,224 canonical imports, the complete original feature patch and all unrelated full-prefix files/pins preserved. All 38 files in the local dependency closure remain unchanged from the audited main context. This exact candidate has actually landed (reported merge time 2026-10-31, 04:19:46 UTC); ancestry and all three reviewed payloads were independently checked on actual main. Successful cumulative MQ 41167200396 passed all six gates at exact descendant ecfdc535. Its sole finalized-log receipt was reused after independently checking the checkout/tree, ancestry, original payloads, all 38 local dependency files and pins. Individual MQ 41167198398 was unfinished when cumulative coverage was accepted; it is not claimed successful. The fixed covering main consumer also passed all six gates at exact ecfdc535 and published at 04:34:49.9493813 UTC. The sole public-cache audit verifies 4,304 unique map entries and all 29 new artifact references returning HEAD 200 with positive lengths. Its saved log, map and baseline chain were reused with zero duplicate requests or artifact bodies. The optional producer handoff was unavailable; main built 47 Complexity modules and passed validation, so no restore-success claim is made. Source, current review, native coverage, actual landing and usable-cache follow-through are complete.