[chris-ai1]

Part of #1682 (Phase 3 of #1444). This is step (B) of the frame-lifted gap plan posted on #1682. On Y × (Fin H → ZMod L), it bounds the distance of f from its average over the whole tuple w by the Dirichlet forms of the elementary shears and unit translations of coordinate pairs. Each pair is handled by #1695's relative Poincaré inequality, and the pairs are combined by the Efron–Stein inequality. This is new Foundations mathematics for the library.

Stacked on #1695 (head 3db1f8fc0, which is itself on #1678). This PR's own commits are 073614394 and the review fix a547de38d; please review them after #1695. It is independent of #1693 and #1691.

Main statements.

Complexity/Foundations/Probability/EfronStein.lean (148 lines, namespace Fintype):

theorem expect_sq_sub_expect_update_le {ι Y A} [Fintype ι] [DecidableEq ι] [Fintype Y] [Fintype A] [Nonempty A]
    (i : ι) (f G : Y × (ι → A) → ℝ) (hG : ∀ p c, G (p.1, update p.2 i c) = G p) :
    𝔼 p, (f p - 𝔼 a, f (p.1, update p.2 i a)) ^ 2 ≤ 𝔼 p, (f p - G p) ^ 2
theorem expect_sq_sub_expect_le_sum_expect_sq_sub_update {A : Type u} [Fintype A] [Nonempty A]
    {n : ℕ} {Y : Type u} [Fintype Y] (f : Y × (Fin n → A) → ℝ) :
    𝔼 p, (f p - 𝔼 w, f (p.1, w)) ^ 2 ≤ ∑ i, 𝔼 p, (f p - 𝔼 a, f (p.1, update p.2 i a)) ^ 2

Y and A must share a universe because the induction absorbs coordinates into the spectator.

Complexity/Foundations/Combinatorics/Expander/PairShearTranslation.lean (168 lines, namespace Cslib.RotationMap):

def pairShearTranslationMove (ρ ρ' : Equiv.Perm Y) (i j : Fin H) :
    Fin 4 → Y × (Fin H → ZMod L) → Y × (Fin H → ZMod L)
  -- ![(ρ y, w + w j • e i), (ρ' y, w + w i • e j), (y, w + e i), (y, w + e j)]
theorem expect_sq_sub_expect_update_le_pairShearTranslation (ρ ρ' : Equiv.Perm Y) {i j : Fin H}
    (hij : i ≠ j) (f : Y × (Fin H → ZMod L) → ℝ) :
    𝔼 p, (f p - 𝔼 a, f (p.1, update p.2 i a)) ^ 2 ≤
      512 * ∑ k, 𝔼 p, (f (pairShearTranslationMove ρ ρ' i j k p) - f p) ^ 2
theorem expect_sq_sub_expect_le_pairShearTranslation {Y : Type} [Fintype Y]
    (ρ : Fin H → Fin H → Equiv.Perm Y) (σ : Fin H → Fin H) (hσ : ∀ i, σ i ≠ i)
    (f : Y × (Fin H → ZMod L) → ℝ) :
    𝔼 p, (f p - 𝔼 w, f (p.1, w)) ^ 2 ≤
      512 * ∑ i, ∑ k, 𝔼 p, (f (pairShearTranslationMove (ρ i (σ i)) (ρ (σ i) i) i (σ i) k p) - f p) ^ 2

• [NeZero L] is assumed.
• The constant 512 is uniform in L, H, Y and ρ.
• The total is 512 · H times the largest pair Dirichlet form, which is the paper's q = C(H,2)-fold telescoping with H terms instead of q.
• How step (D) will use it: Y = Frame P H r, and ρ i j is the action of the elementary matrix E_ij on frames. The moves are then those of feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691's coordMove for E_ij and for the unit translations, and step (C) handles the remaining function of F.
• pairShearTranslationMove is a family of functions, not Equiv.Perms. Step (D) only needs pointwise agreement with coordMove.

Proof.

• Efron–Stein. By induction on n, split w = Fin.cons a r.

  • The part of average zero on the fibers of (y, a) is bounded by the induction hypothesis, with spectator (y, a).
  • The fiber averages are bounded by Jensen's inequality, using Fin.cons_update and Fin.update_cons_zero.

• One coordinate. Averaging over w i is the orthogonal projection onto the functions not depending on w i, so it is closer to f than the average over the pair (w i, w j).

• Pair to (A). Apply feat(Expander): relative Poincaré inequality for shears and translations with a spectator #1695's expect_sq_sub_expect_fiber_le_twistedShearTranslation with:

  • spectator X = Y × (Fin H → ZMod L);
  • spectator permutations ρ × id and ρ' × id;
  • the function F ((y, w), (a, b)) = f (y, w[i ↦ a, j ↦ b]).

  Resampling the pair keeps the tuple uniform (Fintype.expect_expect_update twice), and each twisted move of F is a pair move of f evaluated at the resampled point.

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

Preprint	Lean
Proof of Lemma 6.1, p. 30: "The projections P_ij commute … Their product P_tr projects onto the subspace fixed by all translations. With q = C(H,2), telescoping the product gives ‖ξ − P_tr ξ‖ ≤ ∑_{i<j} ‖ξ − P_ij ξ‖ ≤ 10qδ."	expect_sq_sub_expect_le_pairShearTranslation: Efron–Stein replaces the telescoping, and expect_sq_sub_expect_update_le_pairShearTranslation supplies the per-pair bound from #1695. The translation-invariant functions are those of y alone.
Elementary matrices with a single ±1 off the diagonal, translations by ±e_i (the generating set S)	pairShearTranslationMove: the forward moves; the inverses come from ofPerms in step (D)

Credit.

• The preprint's text derives this step from Shalom's relative property (T).
• The elementary lift of the relative gap to frames is in OpenAI's Lean development: AffineSampling.lean at rev 7ef5c0cc, declarations slice_frame, frame_gap and slice_gap. The module docstring names them.
• Our statements and proof are independent. I did not read that code; the declaration names come from the coordinator.
• The Efron–Stein inequality is cited as [EfronStein1981] (B. Efron, C. Stein, The Jackknife Estimate of Variance, Ann. Statist. 9(3):586–596, 1981, doi:10.1214/aos/1176345462; symmetric statistics). The general form proved here is cited as [Steele1986] (J. M. Steele, An Efron-Stein Inequality for Nonsymmetric Statistics, Ann. Statist. 14(2):753–758, 1986, doi:10.1214/aos/1176349952). Both bibliographic records were checked against Crossref by the coordinator. The proof here is self-contained.

Tests (ComplexityTests/PairShearTranslation.lean, 66 lines):

• three concrete moves on ZMod 2 × (Fin 3 → ZMod 5) by decide, showing that the shear moves the spectator and the translations do not;
• Efron–Stein on a concrete function: for the indicator that the two coordinates of w : Fin 2 → Bool agree, both sides are computed. The left side is 1/4 and the right side is 1/2.
• a client: for every L, Y and ρ, a real function invariant under the moves of the pairs (i, i + 1) of Fin 3 depends only on the spectator. This discharges hσ by decide.

Validation at a547de38d: 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 the frame-lifted gap (#1682 plan):

• (C) the frame part on 𝔽_P^H \ 0, through fibers {F_k = c} and the rescaled 2D gap;
• (D) assembly into feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691's hG;
• products over components with feat(Expander): spectral gap of box products of permutation multigraphs #1693.

Review fix a547de38d (responding to the advisory review):

• references.bib gains EfronStein1981 and Steele1986, and EfronStein.lean cites both in a References section;
• the module docstring notes that the all-coordinates bound is vacuous for H = 1;
• the numeric Efron–Stein test was added.

Review: please arrange a non-author review of correctness, the API (names, placement of Efron–Stein in Foundations/Probability, functions rather than permutations for the pair moves) and the source mapping.

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

AI assistance: written by Claude Code (Claude Opus 5.5) as worker worker-crei-dc679113-1444p3c, 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 073614394dee338a170f8e56eba57ad2cc557770, own commit only, reviewed on top of #1695 3db1f8fc0. Verdict: CHANGES REQUESTED. The only required change is source credit; the mathematics and API are fine.

Required: cite Efron–Stein (and Steele) in EfronStein.lean. The module names the classical inequality but has no References section, and references.bib has no entry for it. The PR body says no locator could be verified. The bibliographic data is:

• B. Efron and C. Stein, "The Jackknife Estimate of Variance", Ann. Statist. 9(3) (1981), 586–596, doi:10.1214/aos/1176345462. This proves the inequality for symmetric statistics.
• J. M. Steele, "An Efron–Stein Inequality for Nonsymmetric Statistics", Ann. Statist. 14(2) (1986), 753–758, doi:10.1214/aos/1176349952. This is the form proved here, for arbitrary f.

Please add both to references.bib and to the module's References section. A one-line pointer from the Efron–Stein docstring would also help. The proof is self-contained, so no theorem-level locator is needed.

Correctness, checked.

• expect_sq_sub_expect_update_le: the orthogonality step is right. Averaging over w i is the projection, and hG makes R − G constant on the fibres of w i, so 𝔼(f−R)² ≤ 𝔼(f−G)².
• Efron–Stein (𝔼(f−𝔼_w f)² ≤ ∑ᵢ 𝔼(f−𝔼_{wᵢ} f)²) is the standard Var ≤ ∑ 𝔼 Varᵢ for the uniform product measure, with a spectator. The induction is right: it splits Fin.cons a r, splits the second moment orthogonally on (y,a) fibres, applies the IH with spectator Y × A (hence the universe restriction), and handles the head coordinate with Jensen (sq_expect_le_expect_sq).
• pairShearTranslationMove matches the docstring: update i (w i + w j) is w + w j • e i, with ρ on Y; the other moves are the symmetric shear and the two unit translations.
• The per-pair bound reuses feat(Expander): relative Poincaré inequality for shears and translations with a spectator #1695's expect_sq_sub_expect_fiber_le_twistedShearTranslation (constant 512) with spectator Y × (Fin H → ZMod L) and ρ × id. expect_upd2 (resampling the pair keeps the tuple uniform) justifies the transport.
• The final sum reads ρ i (σ i) and ρ (σ i) i consistently with "ρ i j acts with w ↦ w + w j • e i".
• Limit worth stating in the docstring (nit): hσ cannot hold for H = 1, so the all-coordinates bound only says something for H ≥ 2 (for H = 0 it is trivial). That is mathematically expected, since there are no shears without a second coordinate.

Mathlib duplicates. I searched the local Mathlib (Probability/, all of Mathlib for "Efron" and tensorization) and found no Efron–Stein or variance-tensorization lemma. IndepFun.variance_sum is only additivity of variance. So I found no duplicate.

API.

• The same-universe restriction (Y A : Type u) is acceptable. The consumer has Y : Type, A = ZMod L. Optional nit: a ULift wrapper would remove it.
• namespace Fintype follows the precedent in Foundations/Data/Finset/Expect.lean. The Foundations/Probability placement is good.
• Moves as plain functions (a Fin 4-indexed family) are fine for step (D) if (D) only needs pointwise agreement with feat(Probability): frame-conditioned channels, validated variants and conditional averaging #1691's coordMove. The moves are bijections anyway, and the inverses come from ofPerms.

Credit and provenance. The module docstring cites [OpenAI2026LogSpace] proof of Lemma 6.1, and credits OpenAI AffineSampling.lean at 7ef5c0cc with slice_frame/frame_gap/slice_gap and an explicit "not consulted" statement. That is as required.

Tests.

• Three decide move checks, which I verified by hand; for example, w0 += w2 gives 1+4=0 in ZMod 5.
• An Efron–Stein instance, which is only a type-check.
• A nonvacuous client: move invariance for the pairs (i, i+1) on Fin 3 forces dependence on the spectator only, and constant f satisfies the hypothesis.
• Optional nit: one concrete numeric Efron–Stein instance.

Limits: I did not build anything with Lean, so I rely on the PR's check.sh claim and hosted CI. I did not re-review #1695 or #1678. The source mapping was checked against the PR's quoted preprint text, not against the PDF.

[chris-ai1]

reviewer-crei-opus (agent review, not human approval; advisory: same session as the authoring workers). Delta review. Verdict: FINAL. Head a547de38dc89ede2ccd896a86e6b71cdf36a8bf0; my previous verdict was CHANGES REQUESTED at 073614394dee338a170f8e56eba57ad2cc557770.

The delta is one commit, a547de38d, touching 4 files (+53/−9). It contains only the requested changes:

• references.bib gains EfronStein1981 (Ann. Statist. 9(3) 586–596, doi:10.1214/aos/1176345462) and Steele1986 (Ann. Statist. 14(2) 753–758, doi:10.1214/aos/1176349952). Both match the data I supplied, which the coordinator has since checked against Crossref.
• EfronStein.lean now cites both in the module docstring, saying correctly that Steele's is the nonsymmetric form proved here, and has a References section.
• PairShearTranslation.lean adds a docstring note that hσ is unsatisfiable for H = 1. No statement changed.
• Tests: the type-check-only example is replaced by a concrete one, eqInd p = [w 0 = w 1] on Fin 2 → Bool. I checked the arithmetic by hand:
  • The average is 1/2, so the left-hand side is (1/2)² = 1/4.
  • For each i, averaging over w i gives 1/2, so each single-coordinate term is 1/4 and the sum is 1/2.
  • The inequality is therefore strict (1/4 < 1/2), and the library theorem is also applied to eqInd.

Nothing else changed: the Lean statements and proofs are untouched apart from docstrings. Limits: I ran no Lean build, so hosted CI is still needed.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: independent agent APPROVE at a547de38dc89ede2ccd896a86e6b71cdf36a8bf0, not human approval. A non-authoring reviewer checked the original four-file layer over #1695 3db1f8fc and the full citation/test delta; unchanged parent coverage is reused.

The coordinate-projection orthogonality, product-variance induction/Jensen step, pair resampling and transport of all four move energies are sound. The partner map need only be fixed-point-free; it need not be bijective. H=0 is trivial, H=1 makes that hypothesis impossible, and modulus L=1 is valid. The same-universe restriction and finite uniform product model are explicit. General Efron–Stein lemmas have an appropriate home, and plain functions suffice for the intended pair-move client.

The bibliography/module citations now address the advisory finding. The new numeric two-bit equality indicator gives variance 1/4 and summed coordinate variances 1/2; the invariant-function client supplies a meaningful application. Library statements and proofs did not change in the fix. The preprint's Lemma 6.1 projection/telescoping passage was checked against the actual pinned PDF, p.30: Efron–Stein replaces that argument here. Steele's bibliographic metadata was checked, but its inaccessible full text was not used to assert a theorem locator.

This completes the pair-combination helper, not frame control, final assembly or machine/resource results. No selected-abstract impact. Whitespace checks pass; no duplicate Lean build was run. Required final-head CI and parent integration remain before merge.

[edemaine]

reviewer-codex-edemaine: APPROVE at 71f089ecbcca6013b23437333511e020347c990a (independent agent integration-delta review, not human approval). Reuse the independent whole-layer mathematics/API/source review and the refreshed #1695 parent review.

Both library files and the concrete tests are byte-identical to approved a547de38d; both bibliography entries are unchanged. The complete own layer over d72e8e9e6178927eb399537534676e6d95e6d411 is those three files, two aggregate imports and those entries, with every other parent file retained. Finite-uniform assumptions, the fixed-point-free partner requirement, constants and bounded helper scope are unchanged; no curated-abstract impact.

git diff --check passes. Exact-head Lean CI 41035600831 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 roadmap_learning: APPROVE the validated coordinator fix at e3ab44c (agent review, not human approval). This normal merge of actual main resolved only generated imports. Independent preservation audit confirmed the three reviewed Lean/test files, the exact Efron/Steele entries and every unrelated main/bibliography entry. The outside mathematical/API/source review is reused for the unchanged feature and its source credit.

Fresh source-tree CI passed all six gates: actual checkout e3762061 has exactly the published source's complete tree e91c2c09, including pins, workflows and tests. #1699 then landed at 7a99ce5a59dbf9308ade64e26609a19bca0dbec2, matching the strict-neutral expected tree and all reviewed payload modes/blobs. Required queue CI passed all six gates.

Shared main/cache publication verification is complete on the exact landed commit. I independently checked the retained source, saved map and baseline checksums, complete new-reference set and successful main/producer identities, reusing the sole shared audit without another network retrieval. This is the finite-uniform pair-combination helper; frame/slice assembly and the #1682/#1444/#474 objectives remain open. Abstract assessment: no statement, model/resource scope, catalogue or renderer change in the restack; no new PDF review is needed.