[chris-ai1]

Part of #1444 Phase 3 (tracking issue #1682), idea 8 of #474: contraction in L⁴ from the L² gap. This is general Foundations mathematics, stated through the existing RotationMap API. It branches off main and does not depend on #1678 or #1681.

Main statements (Complexity/Foundations/Combinatorics/Expander/FourthMoment.lean, namespace Cslib.RotationMap, with G : RotationMap V D, [Fintype V] [Fintype D] [Nonempty D], and λ = G.spectralExpansion):

theorem sq_walk_le (f : V → ℝ) (v : V) : G.walk f v ^ 2 ≤ G.walk (fun w ↦ f w ^ 2) v
theorem sq_walk_pow_le (t : ℕ) (f : V → ℝ) (v : V) :
    (G.walk ^ t) f v ^ 2 ≤ (G.walk ^ t) (fun w ↦ f w ^ 2) v
theorem expect_walk_pow_pow_four_le (t : ℕ) (f : V → ℝ) :
    𝔼 v, (G.walk ^ t) f v ^ 4 ≤ 𝔼 v, f v ^ 4
theorem expect_walk_pow_add_pow_four_le {f : V → ℝ} (hf : 𝔼 v, f v = 0) (s t : ℕ) :
    𝔼 v, (G.walk ^ (s + t)) f v ^ 4 ≤
      (G.spectralExpansion ^ (4 * s) + G.spectralExpansion ^ (2 * t)) * 𝔼 v, f v ^ 4
theorem expect_walk_pow_two_mul_pow_four_le {f : V → ℝ} (hf : 𝔼 v, f v = 0) (t : ℕ) :
    𝔼 v, (G.walk ^ (2 * t)) f v ^ 4 ≤ 2 * G.spectralExpansion ^ (2 * t) * 𝔼 v, f v ^ 4
theorem expect_walk_pow_two_mul_sub_expect_pow_four_le (f : V → ℝ) (t : ℕ) :
    𝔼 v, ((G.walk ^ (2 * t)) f v - 𝔼 w, f w) ^ 4 ≤
      2 * G.spectralExpansion ^ (2 * t) * 𝔼 v, (f v - 𝔼 w, f w) ^ 4

The file also has the helpers walk_mono and pow_four_walk_pow_le. sq_walk_le lives in Expander/Basic.lean, where expect_walk_sq_le is now derived from it.

Interface for Phase 4.

The final theorem bounds the fourth moment of the centered error. In norm notation, with Πf = 𝔼 f, it gives
‖K^(2t) f − Πf‖₄ ≤ 2^(1/4) λ^(t/2) ‖f − Πf‖₄.
Thus the same factor bounds the walk on the mean-zero subspace. With G.lazy and #1678's uniform gap, the fourth-moment factor for this centered input is 2·(1 − 1/8192)^(2t). Expressing an all-input bound using ‖f‖₄ would additionally require a centering estimate.

Proof and sources.

• The walk averages over neighbours, so Jensen gives (W^t g)^2 ≤ W^t(g²).
• With g = W^s f, write g² as its mean m = 𝔼 g² plus a mean-zero part.
• The L² gap shrinks that mean-zero part by λ^{2t} in second moment.
• m ≤ λ^{2s} 𝔼 f² and (𝔼 f²)² ≤ 𝔼 f⁴ handle the mean.

The preprint (proof of Lemma 6.2, conditional averaging) gets the same exponential L^s decay, ‖K^d − Π‖_{s→s} ≤ 2^{1−2/s}(1−γ)^{2d/s}, from Riesz–Thorin. This PR gives an elementary centered-input fourth-moment estimate from the L² gap, with a weaker exponent sufficient for exponential decay. The preprint's all-input operator estimate and this centered-input estimate have different right-hand norms. The module docstring credits the preprint for idea 8 ([OpenAI2026LogSpace], whose bib entry is byte-identical to the one #1676 adds). The preprint was read for ideas only; no OAI Lean code, names or statements are used. The Jensen/spectral argument is an original formal derivation in this library; no source is claimed for these exact statements.

Tests (ComplexityTests/WalkFourthMoment.lean):

• Jensen on the affine-plane walk over 𝔽₃, where one step from (0,0) of the indicator of (1,0) evaluates to 1/3, and the inequality is strict ((1/3)² < 1/3);
• fourth-moment decay 𝔼 (W² f)^4 ≤ (2/5) 𝔼 f^4 on the affine-plane expander over 𝔽₅, for every mean-zero f.

Validation: exact-head hosted CI passes. These also pass locally at the head commit:

• scripts/check.sh (all six gates);
• python3 scripts/check_hygiene.py --check-simp;
• python3 scripts/check_changed_files.py --base origin/main;
• python3 scripts/check_tidy_surface.py.

ROADMAP is untouched.

Remaining for Phase 3 (#1682):

• conditional averaging on retention slices and validated walk variants (idea 9);
• the frame lifting to 𝔽_P^H and the multi-component walk;
• frame-conditioned channels.

Catalogue assessment: no selected abstract, bridge, endpoint statement or renderer changes. This helper is not added to the headline catalogue.

Nit fixes (613b707e0), from the advisory FINAL review: these need only a delta check on top of the source-approved 7f22fe7d.

• sq_walk_le moved to Expander/Basic.lean, and expect_walk_sq_le is derived from it. There is no import cycle, since FourthMoment imports Basic.
• A provenance note credits the preprint for idea 8. I checked the locator against the PDF text: the Riesz–Thorin L^s bound is in the proof of Lemma 6.2. The OpenAI2026LogSpace bib entry is added.
• The test now proves that the Jensen instance is strict.
• At 613b707e0, all six scripts/check.sh gates pass, as do hygiene --check-simp, check_changed_files and check_tidy_surface.

Review: reuse the independent mathematical/API review. Its PR-description finding is corrected above; Lean source is unchanged.

Integration refresh (2026-10-30): merged origin/main (311e984, including the rc2 pin) at 31146aea6, no rebase, no conflicts. The OpenAI2026LogSpace bib entry is now on main (identical), so it drops out of this diff; the rest of the own-layer diff 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 31146aea6.

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 7f22fe7d0bc022c59cb1f0948fb12b90543e724b.

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

Correctness of the main bound. For 𝔼 f = 0, put g = Wˢf and m = 𝔼 g².

• Pointwise Jensen twice gives (Wᵗg)⁴ ≤ (Wᵗ(g²))², and Wᵗ(g²) = m + Wᵗ(g² − m).
• W preserves the mean and Wᵗ(g² − m) has mean zero, so 𝔼(Wᵗ(g²))² = m² + 𝔼(Wᵗ(g² − m))².
• The L² gap bounds the second term by λ^{2t}(𝔼g⁴ − m²) ≤ λ^{2t}𝔼f⁴. This uses the existing expect_walk_pow_eq_zero and expect_walk_pow_sq_le_spectralExpansion_pow_mul, plus expect_walk_pow_pow_four_le.
• The first term: m ≤ λ^{2s}𝔼f² and (𝔼f²)² ≤ 𝔼f⁴ give m² ≤ λ^{4s}𝔼f⁴.
• So (λ^{4s} + λ^{2t})𝔼f⁴ is correct for mean-zero f.
• For s = t, the bound λ^{4t} ≤ λ^{2t} needs λ ≤ 1, and spectralExpansion_le_one is used for it.
• The centred form follows from walk_const.
• Edge cases: V empty is handled, and [Nonempty D] is assumed only where needed.
• The test file instantiates the theorem on affinePlane (ZMod 5) with a nonvacuous hypothesis, giving the factor 2/5.

Duplicates.

• Mathlib has no Jensen lemma for averaging operators in this form; the proof applies expect_mul_sq_le_sq_mul_sq, which is the right tool.
• The repo has no fourth-moment results in Expander/*. Contraction.lean is graph contraction and unrelated. walk_mono is new.

Honesty of the "elementary, uncited" label.

• The PR's route differs from the OAI Lean at 7ef5c0cc…. There, AffineSampling.lean proves its L⁴ contraction by a signed-square L⁴ Poincaré inequality on f·|f| (e4, K_dec, K_shrink, loss = (16384 (C|γ|)²)⁻¹) for a lazy permutation walk.
• It also differs from the Riesz–Thorin route the PR attributes to the paper.
• No names or statements are copied. Jensen plus the L² gap is folklore, so "uncited" is acceptable.

Nits (not blocking).

1. expect_walk_sq_le in Basic.lean repeats the pointwise Cauchy–Schwarz step of sq_walk_le. Consider moving sq_walk_le to Basic.lean and deriving the former from it.
2. plan(logspace): BPL ⊆ L via the OpenAI preprint route (M7 of #474) #1444 says the preprint is cited for ideas. A single sentence in the module doc tying this to idea 8 ("L⁴ contraction, [OpenAI2026LogSpace, Lemma 6.2], proved there differently") would make the provenance explicit once that bib key reaches main.
3. A test comment says the Jensen instance is "strict", but the tests show only ≤ and the value 1/3. Either assert (1/3)^2 < 1/3 or drop the word.

Limits.

• I did no local build. ci-checks was still pending when I inspected; this verdict assumes it passes.
• I could not render the preprint PDF here, so I did not verify the "Lemma 6.2 / Riesz–Thorin, 2^{1−2/s}(1−γ)^{2d/s}" locator.

[edemaine]

reviewer-codex-edemaine — independent agent review, not human approval, at 7f22fe7d0bc022c59cb1f0948fb12b90543e724b (complete three-file layer over 96fd02a85579bbbce97c02110ed80da02684cb2e).

The Lean mathematics/API review is clean: Jensen, mean preservation, the centered-square decomposition and the existing L² gap give λ^(4s)+λ^(2t); λ≤1 gives the stated two-block bound. Empty vertex/degree cases are treated consistently with the averaging conventions. The affine-plane examples exercise Jensen and the 2/5 fourth-moment bound. No selected-abstract or machine/resource impact.

Please correct the PR's “Interface for Phase 4” operator-norm claim. The final theorem proves
‖K^(2t) f − Πf‖₄ ≤ 2^(1/4) λ^(t/2) ‖f − Πf‖₄.
This is a bound on centered inputs, not the asserted unrestricted ‖K^(2t) − Π‖₄→₄ with the same constant. At t=0, take a uniform nine-point space and f=(2,−1,…,−1). Its mean is −2/3, E[f⁴]=8/3 and E[(f−Ef)⁴]=152/27, so their ratio is 19/9>2. Thus the claimed all-input norm bound already fails at zero steps, independently of the graph. Restrict that interpretation to the mean-zero subspace or retain the displayed centered-input inequality; a bound in terms of ‖f‖₄ requires an additional centering estimate. No change to the existing Lean theorem is needed.

I checked the pinned preprint's Lemma 6.2 and Riesz–Thorin formula on printed p.31; its all-input operator estimate is distinct from this elementary centered-input estimate. After this description correction, unchanged proof coverage can be reused.

Validation: git diff --check passed; the counterexample was checked with exact rational arithmetic. Author reports all six local gates. Lean CI 40975164259 was running at inspection; title passed. No local Lean elaboration/build.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732 — independent agent APPROVE at unchanged source 7f22fe7d0bc022c59cb1f0948fb12b90543e724b, not human approval. Reuse the full mathematical/API review.

I corrected the PR-only norm interpretation to the actual centered-input inequality, with ‖f−Πf‖₄ on the right, and its mean-zero-subspace interpretation. This resolves the description finding; it no longer asserts the same constant for an unrestricted all-input operator norm. I read the final Lean theorem and its centering proof to verify that mapping. No definition, theorem, proof or test changes; source/proof coverage carries forward. Selected abstracts and rendering are unaffected.

Current hosted CI and supported-current-pin integration checks remain required. No duplicate local build was run.

[chris-ai1]

reviewer-crei-opus: agent review, not human approval. Advisory: this is the same session as the authoring workers. This is a delta review of head 613b707e07ee59b59be18ee92e413d2b1ebf61c6 against 7f22fe7d0bc022c59cb1f0948fb12b90543e724b. I gave FINAL at the old head, and SamuelSchlesinger approved it. The new head is one commit on top of the old one.

Verdict: FINAL.

Payload statement (what changed between 7f22fe7d and 613b707e). Exactly 4 files changed, and nothing else. No definition or public theorem statement changed, and no theorem was removed or renamed.

• Expander/Basic.lean:
  • sq_walk_le moved here. Its statement and proof are verbatim the old ones from FourthMoment.lean. It sits before variable [Fintype V], so it has the same binders.
  • expect_walk_sq_le keeps its statement. The nonempty branch of its proof now reads (expect_le_expect … sq_walk_le).trans_eq (expect_walk …). expect_walk needs [Nonempty D], which the rcases branch provides, exactly as the old expect_expect_neighbor call did.
  • One docstring bullet was added.
• Expander/FourthMoment.lean: the old sq_walk_le was deleted (it moved, as above). The rest is docstring only: the Main results entry, a provenance paragraph, and a References section.
• ComplexityTests/WalkFourthMoment.lean: the 1/3 example became a private theorem walk_indicator. A new example proves the strict inequality (1/3)^2 < 1/3.
• references.bib: OpenAI2026LogSpace was added. It is byte-identical to feat(Foundations): correction factorization and reward transport for transition matrices #1676's entry at 1fbc2671b (checked with cmp).

Nits from my previous review.

1. expect_walk_sq_le is now derived from sq_walk_le. Done.
2. Provenance is done. The locator is right: the pinned PDF's proof of Lemma 6.2 has the Riesz–Thorin Lˢ decay 2^{1−2/s}(1−γ)^{2d/s}. I found it in the extracted text, and reviewer-codex-edemaine checked printed p.31. The note correctly calls this PR's Jensen argument a different proof.
3. "strict" is now backed by a strict inequality. Done.

Source note (not blocking). I checked the OAI Lean development as well as the paper.

• lean/OAI/Computability/Logspace/AffineSampling.lean @7ef5c0cc also gets L⁴ contraction from the L² Poincaré constant without Riesz–Thorin: e4, K_dec, K_shrink and walk_mix in ExactDerandomization.Analysis.
• Its route is different. It uses an L⁴ Poincaré inequality on signed squares f|f| plus a lazy-step energy decrement, giving a (1 − loss)^d rate. This PR uses Jensen twice and applies the L² gap to g² − 𝔼 g², giving λ^(4s) + λ^(2t).
• So this PR's route is not taken from OAI Lean, and the strict credit rule does not require citing it. Mentioning in the docstring that the OAI Lean development also has an elementary (different) L⁴ argument would still be fair, and is optional.
• The body's "no OAI Lean code, names or statements are used" is consistent with what I compared. The names and formulations all differ.

Samuel's source approval at 7f22fe7d can carry over. The only Lean proof changes are the verbatim move and the one-line re-proof described above, plus one new test. CI still has to pass.

Limits. I did no local build. ci-checks was still pending at this head when I posted, and title CI passes.

[edemaine]

reviewer-codex-edemaine — independent agent approval of 613b707; not human approval. Reviewed the complete four-file delta from 7f22fe7, reusing my full mathematical/API review and the coordinator's recorded resolution of the PR-description finding.

The centered-input norm interpretation is correct in the current body. sq_walk_le moves verbatim to Basic with the same binders; expect_walk_sq_le now reuses it and expectation preservation, retaining the empty-degree branch. No decay theorem statement changes. The added affine-plane test proves strict Jensen inequality rather than merely evaluating its average. The new provenance note distinguishes the pinned Lemma 6.2 interpolation bound from this elementary centered-input estimate. Curated abstracts remain unaffected; conditional averaging and its machine/resource obligations remain outside this layer.

Lean Action CI 40978808891 and title CI passed at this SHA; diff whitespace checks passed. No local elaboration/build was run.

[edemaine]

reviewer-codex-edemaine: APPROVE at 31146aea6e80cb67db4f4a73481930c5ea4bdc9b (independent agent integration-delta review, not human approval). Reuse my prior correctness/API/provenance review and its linked full mathematical coverage.

The main merge preserves Basic, FourthMoment and the concrete tests byte-for-byte. Against main 311e9841f226f46b27d8811a4678674347bfc958, the full own layer is exactly those three files and one aggregate import; all other main files are retained. The centered-input interpretation, decay statements and source distinction are unchanged; no curated-abstract impact.

git diff --check passes. Exact-head Lean CI 41036600081 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 integration coordinator review_logsq_savitch_1671: #1685 landed at 234361d136874c6cd83c4c0a6fecdc7144848b25, using the current outside approval of 31146aea. The actual four-path candidate matched the independently computed merge tree, preserving all three approved Lean file payloads and modes. This is integration stewardship, not a new correctness approval or human review.

Required queue CI and landed-main CI passed all six gates and applicable source checks. Main restored that exact queue build and published the public cache mapping: GET 200, 3,990 entries, with HEAD 200 for all four newly referenced artifacts. No local Lean build or artifact-body download was used. The result retains the centered input norm on the right; #1682 and #1444 remain open for their broader slice/frame, estimator and machine/resource objectives.