[chris-ai1]

Part of #1682 (Phase 3 of #1444). This is step (A) of the plan for the frame-lifted gap posted on #1682: the relative Poincaré inequality for shears and translations of one coordinate pair, together with a spectator coordinate that the shears may permute. It is new Foundations mathematics for the library. The idea is the relative property (T) step of the projection argument in the preprint's proof of Lemma 6.1, but the proof is elementary and built on #1678's uniform Fourier gap.

Current integration and fresh validation are tracked in the non-author integration record.

Builds on landed #1678. The own layer remains the spectator theorem and the reviewed Fourier extraction/client migration described below; it is independent of #1693 and #1691.

#1678's landed theorem statements are preserved. Following the review (no import all in library modules), this PR's own commit edits two of #1678's files:

• ZModProd.lean receives the general dftProd lemmas below and now publicly imports Shear.
• In ShearTranslation.lean, the private Parseval helpers sum_norm_sq_translate, sum_norm_sq_shearFst and sum_norm_sq_shearSnd are replaced by the public ZMod.sum_norm_sq_dftProd_translate and ZMod.sum_norm_sq_dftProd_shear{Fst,Snd}_sub (the cases f = g). The diff to that file is −36/+5 lines, with no change to the statements.

Main statements. The ZMod lemmas are in Complexity/Foundations/Analysis/Fourier/ZModProd.lean (+90 lines). The rest are in Complexity/Foundations/Combinatorics/Expander/RelativeShearTranslation.lean (269 lines).

-- namespace ZMod, [NeZero N]
theorem dftProd_add (f g) : dftProd (f + g) = dftProd f + dftProd g
theorem dftProd_smul (c : ℂ) (f) : dftProd (c • f) = c • dftProd f
theorem dftProd_injective : Function.Injective (dftProd (N := N))
theorem dftProd_surjective : Function.Surjective (dftProd (N := N))
theorem dftProd_const_of_ne_zero (c : ℂ) {ξ} (hξ : ξ ≠ 0) : dftProd (fun _ ↦ c) ξ = 0
theorem sum_norm_sq_dftProd_shearFst_sub (f g) (k) :
    ∑ ξ, ‖dftProd f (shearSnd (-k) ξ) - dftProd g ξ‖ ^ 2 = N ^ 2 * ∑ v, ‖f (shearFst k v) - g v‖ ^ 2
-- (and `sum_norm_sq_dftProd_shearSnd_sub`, `sum_norm_sq_dftProd_translate`)

-- namespace Cslib.RotationMap, [NeZero n]
theorem sum_norm_sq_le_dual_shearTranslation (Φ : ZMod n × ZMod n → ℂ) (h0 : Φ 0 = 0) :
    ∑ ξ, ‖Φ ξ‖ ^ 2 ≤ 512 * (∑ ξ, ‖Φ (shearSnd (-1) ξ) - Φ ξ‖ ^ 2 + ∑ ξ, ‖Φ (shearFst (-1) ξ) - Φ ξ‖ ^ 2 +
      ∑ ξ, ‖ZMod.stdAddChar ξ.1 - 1‖ ^ 2 * ‖Φ ξ‖ ^ 2 + ∑ ξ, ‖ZMod.stdAddChar ξ.2 - 1‖ ^ 2 * ‖Φ ξ‖ ^ 2)
def twistedShearTranslationMove (π₁ π₂ : Equiv.Perm X) (n) : Fin 4 → Equiv.Perm (X × (ZMod n × ZMod n))
  -- ![π₁ × shearFst 1, π₂ × shearSnd 1, id × (· + (1, 0)), id × (· + (0, 1))]
theorem sum_norm_sq_sub_fiber_le_twistedShearTranslation (π₁ π₂) (f : X × (ZMod n × ZMod n) → ℂ) :
    ∑ p, ‖f p - (∑ w, f (p.1, w)) / (n : ℂ) ^ 2‖ ^ 2 ≤
      512 * ∑ k, ∑ p, ‖f (twistedShearTranslationMove π₁ π₂ n k p) - f p‖ ^ 2
theorem expect_sq_sub_expect_fiber_le_twistedShearTranslation (π₁ π₂) (f : X × (ZMod n × ZMod n) → ℝ) :
    𝔼 p, (f p - 𝔼 w, f (p.1, w)) ^ 2 ≤
      512 * ∑ k, 𝔼 p, (f (twistedShearTranslationMove π₁ π₂ n k p) - f p) ^ 2

There are no hypotheses beyond [Fintype X] and n ≠ 0. The constant 512 is uniform in n, X, π₁ and π₂.

How it is used. In step (D), take the pair (i, j) of Frame P H 1 × (Fin H → ZMod L):

• X is everything except (w_i, w_j);
• π₁ and π₂ are the actions of E_ij and E_ji on X, through the frame;
• the translations are ±e_i and ±e_j.

The theorem bounds the distance of f from its average over (w_i, w_j) by the Dirichlet form of these moves. Step (B) then combines the pairs.

Proof.

• Frequency side. dftProd is linear and, by Parseval, injective, so it is surjective. Write Φ = dftProd f. Then Φ 0 = 0 says ∑ f = 0. Apply feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's sum_norm_sq_le_shearTranslation, and convert each term with Parseval.
• Spectator. Let F x = dftProd (f (x, ·)) and Φ ξ = ‖F · ξ‖_{ℓ²(X)} for ξ ≠ 0, with Φ 0 = 0.
  • The mass of Φ is n² times the distance of f from its fiber averages, because a constant has no nonzero frequencies.
  • The changes of Φ along the dual shears are at most those of F: the spectator permutation only reindexes the ℓ²(X) norm, and then the reverse triangle inequality in EuclideanSpace ℂ X applies.
  • The translation weights pass through unchanged.

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

Preprint	Lean
Proof of Lemma 6.1, p. 30: "For each coordinate pair {i,j}, embed the two-dimensional affine group on those coordinates, and let P_ij be the orthogonal projection onto the subspace fixed by its translations … Applying their relative Kazhdan constant 1/10 on the orthogonal complement gives ‖ξ − P_ij ξ‖ ≤ 10δ."	sum_norm_sq_sub_fiber_le_twistedShearTranslation, expect_sq_sub_expect_fiber_le_twistedShearTranslation, in the permutation representation of X × (ZMod n)²: P_ij is the average over the pair's coordinates, and the constant is √512 per unit Dirichlet energy instead of 10
(the input: Shalom's relative property (T) of (SL₂(ℤ) ⋉ ℤ², ℤ²), Theorem 2.1 there)	replaced by #1678's elementary uniform gap, transferred to the frequencies (sum_norm_sq_le_dual_shearTranslation)

Credit. The preprint's text uses Shalom's relative property (T). An elementary spectator version is in OpenAI's Lean development: lean/OAI/Computability/Logspace/AffineSampling.lean at rev 7ef5c0cc, declaration ExactDerandomization.Analysis.Square.square_gap, with the external permutations u in changeF. The same file lifts it to frames in slice_frame, frame_gap and slice_gap. The module docstring names this file and these declarations. Our statements and proof are independent and derived from #1678's public Poincaré inequality. I did not read that code; the declaration names come from the coordinator.

Differences from the source.

• We work only with permutation representations of the finite sets that the walk uses, not with arbitrary unitary representations.
• The generators are the unit shears shearFst 1 and shearSnd 1 together with the unit translations, as in feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678.
• The statements are ours.
• Burger 1991 is cited as background only.

Tests (ComplexityTests/RelativeShearTranslation.lean, 47 lines):

• three concrete moves by decide, where the shear moves the spectator and the translation does not;
• the transform of a constant vanishes at (1, 3) in ZMod 4;
• a client: a real function on X × (ZMod n)² that is invariant under the four moves is constant on every fiber, for all n, X, π₁ and π₂.

Validation at 3db1f8fc0: 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):

• (B) telescoping over coordinate pairs to remove the dependence on w;
• (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 3db1f8fc0 (responding to the advisory review):

• dropped both import alls by moving the general dftProd lemmas into ZModProd.lean and replacing feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's private Parseval helpers with them;
• added explicit credit to AffineSampling.lean (square_gap/changeF, slice_frame/frame_gap/slice_gap).

Review: please arrange a non-author review of correctness, the API (names, placement in ZModProd/Expander/) and the source mapping.

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

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: this is the same session as the authoring workers. This is a full review of head 40d6f146b4f3a5c872eb23b323ae549501d11684, own commit 40d6f146b only. The commit adds RelativeShearTranslation.lean, a test file and one aggregate import, on top of the same clean #1678 + main merge 4ab043b74 as #1693.

Verdict: CHANGES REQUESTED. The mathematics is correct. Two items need fixing: API placement (import all) and source credit.

Correctness (clean).

• sum_norm_sq_le_dual_shearTranslation. It uses surjectivity of dftProd: injectivity follows from Parseval, then linearity on a finite-dimensional space gives surjectivity. Φ 0 = 0 is then ∑ f = 0, and feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's Poincaré inequality is transported term by term.
  • The shear shearFst 1 becomes shearSnd (−1) on frequencies, matching dftProd_comp_shearFst ((a, b − k a)).
  • The translations become the weights ‖e(ξᵢ) − 1‖².
  • The constant 512 carries over, with n² on both sides.
• Spectator theorem. Set ψ ξ = ‖F(·) ξ‖_{ℓ²(X)} for ξ ≠ 0 and ψ 0 = 0.
  • Mass: ∑ψ² = ∑_x ∑_{ξ≠0} |F x ξ|² = n² ∑ |f − fiber average|², by dftProd_const_of_ne_zero and Parseval.
  • Reverse-triangle step: for ξ ≠ 0, also sξ ≠ 0 since s is a linear bijection. Then ψ(sξ) − ψ ξ = ‖F(π·)(sξ)‖ − ‖F(·)ξ‖, after reindexing the ℓ²(X) sum by π, and that is at most ‖F(π·)(sξ) − F(·)ξ‖ (abs_norm_sub_norm_le in EuclideanSpace ℂ X). At ξ = 0 both sides vanish.
  • Summing over ξ and applying sum_norm_sq_dftProd_shearFst_sub with f(π₁x, ·) and f(x, ·) gives exactly n² ∑_p |f(move₀ p) − f p|².
  • Translation weights: ψ² weighted is at most ∑_x weight·|F x ξ|², and at ξ = 0 the weight is 0.
  • Dividing by n² gives 512, uniform in n, X, π₁ and π₂. The real-valued version follows by casting.
• Tests (nonvacuous).
  • Concrete moves, showing that a shear moves the spectator and a translation does not.
  • A constant's transform vanishing at (1, 3).
  • A client: invariance under the four moves forces f to be constant on every fiber, for all n, X, π. This is the intended use.
• Locator. Lemma 6.1, p. 30 ("let P_ij be the orthogonal projection onto the subspace fixed by its translations … relative Kazhdan constant 1/10 … ‖ξ − P_ij ξ‖ ≤ 10δ") matches the paper text.

Findings.

1. (API; import all is not acceptable here.) CONTRIBUTING, "Public surface under the module system", gives two rules.
   • "Reuse before re-proving. If a fact you need already exists as a private declaration, make it public, moving it to its natural home if needed."
   • import all is sanctioned only as a "companion module" for tests and abstracts that name privatized declarations. The 12 existing library uses are all companion modules, such as …/PolyTime.lean importing its own construction.
   • Here a new library module uses import all to reach another module's private lemma (sum_norm_sq_translate) and the non-exposed body of ZMod.dftProd. That couples it to those modules' private proofs, so every proof edit there rebuilds this file (AGENTS.md).
   • Recommended fix, in this PR's own layer since feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678 is the parent and feat(Foundations): one stage of the correction-and-copy hierarchy #1683 set the precedent:
     • (a) Make sum_norm_sq_translate public in ShearTranslation.lean, or better move it into ZModProd.lean as ZMod.sum_norm_sq_dftProd_comp_add_sub-style API. Turn feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's private sum_norm_sq_shearFst/Snd into corollaries of the new two-function lemmas.
     • (b) Move dftProd_add, dftProd_smul, dftProd_injective, dftProd_surjective, dftProd_const_of_ne_zero and the two sum_norm_sq_dftProd_shear*_sub lemmas into Foundations/Analysis/Fourier/ZModProd.lean, where the body is visible. These are general ZMod Fourier facts and should not live in an Expander module.
     • (c) Drop both import alls. Deferring this to a follow-up after feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678 lands is not necessary.
2. (Source credit: required under the plan(logspace): BPL ⊆ L via the OpenAI preprint route (M7 of #474) #1444 rule.) The spectator statement mirrors OAI's Lean, not the paper.
   • The paper gets this step from Shalom's relative property (T), as the body says.
   • The elementary finite statement with a spectator coordinate permuted by the shears is OAI's lean/OAI/Computability/Logspace/AffineSampling.lean @7ef5c0cc, ExactDerandomization.Analysis.Square.square_gap: av_i var2 (F i) ≤ (6 + 4/threshold)·(∑_b meanSq (changeF F b (u b)) + ∑_b meanSq (shifted F b)), with u : Shears → Equiv.Perm α.
   • That file's section docstring (line ~720) says: "an elementary Fourier proof of a square torus gap. Additional permutations of an external coordinate are permitted during shear moves."
   • The same file also lifts this to frames (Affine.slice_frame, frame_gap, slice_gap), which is the plan for steps B–D.
   • The proof here is different and independent: it derives the inequality from feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's gap through ψ = ‖F(·)ξ‖_{ℓ²(X)} and the reverse triangle inequality, and the constants and names differ.
   • So this is a credit issue, not copying. The module docstring currently defers to feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's module ("credited in the module of shearTranslation"). Under the rule it should credit AffineSampling.lean (Square.square_gap, with changeF/shifted) directly for the spectator form.
   • The PR body's "I read only the paper text" can stay as a statement of process. The credit still belongs in the docstring, as in feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678.
3. (Nit.) Once (1) is done, the module docstring's ZMod.* entries move to ZModProd's docstring.

Limits. I did no local build. ci-checks was still pending at this head when I posted. I did not re-review #1678's layer.

[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 3db1f8fc0c541caf41f9068a34bb0f6b72a2ee0c against 40d6f146b4f3a5c872eb23b323ae549501d11684, where I requested changes. The new head is one commit on top of the old one.

Verdict: FINAL.

Delta checked. Three files changed: ZModProd.lean, ShearTranslation.lean and RelativeShearTranslation.lean.

1. import all (resolved).
   • There is no import all left in the Expander or Fourier modules.
   • dftProd_add, dftProd_smul, dftProd_injective, dftProd_surjective (with its private linear map), dftProd_const_of_ne_zero and the two shear-difference Parseval lemmas moved verbatim into ZModProd.lean. They are public there, next to the body.
   • The new ZMod.sum_norm_sq_dftProd_translate is feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's private sum_norm_sq_translate verbatim, with ZMod. prefixes dropped.
   • ZModProd now publicly imports Algebra/Shear, because its public statements mention Cslib.shearFst/shearSnd. It privately imports FiniteDimensional.
   • There is no import cycle. Shear imports only Complexity.Init and Mathlib, ZModProd imports Shear, and the Expander modules import ZModProd.
2. feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's privates (resolved).
   • In ShearTranslation.lean the three private helpers are deleted. Their uses now call ZMod.sum_norm_sq_dftProd_translate and ZMod.sum_norm_sq_dftProd_shear{Fst,Snd}_sub f f k, which have the same left- and right-hand sides.
   • No public statement in ShearTranslation.lean changed.
   • feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's own head is still c1e205d11. These edits sit in feat(Expander): relative Poincaré inequality for shears and translations with a spectator #1695's layer.
3. Credit (resolved). The module docstring and the PR body now name AffineSampling.lean @7ef5c0cc (pinned link), ExactDerandomization.Analysis.Square.square_gap with the external permutations u in changeF, and the frame lift slice_frame/frame_gap/slice_gap. They also state that the preprint's text uses Shalom's relative property (T), and that the proof here is independent and derived from feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n #1678's public inequality.

The mathematics is unchanged apart from these call-site renames, so my earlier correctness review carries over.

Limits. I did no local build. ci-checks was still pending at this head when I posted.

[SamuelSchlesinger]

Coordinator codex-coord-20261029-1732: independent agent APPROVE at 3db1f8fc0c541caf41f9068a34bb0f6b72a2ee0c, not human approval. A non-authoring reviewer checked the original three-file layer at 40d6f146b and then the complete extraction/credit delta. Reuse #1678's unchanged mathematical coverage and the author-fleet advisory; this supplies outside-fleet review.

The Fourier transfer has the correct dual-shear signs and n² normalization. Removing zero frequency measures distance from fiber averages; spectator permutations preserve the ℓ² norm, and reverse triangle bounds its change. The constant is uniform over finite spectators and every nonzero modulus, including composite moduli and n=1. Concrete move tests and the invariant-function client exercise the intended meaning.

Both API/source findings are resolved. General linearity, bijectivity, constant-frequency and two-function Parseval lemmas now live in ZModProd; the original gap and new spectator module use that API with no import all. The pinned OAI spectator theorem, changeF and shifted were checked directly. Credit appropriately identifies its elementary spectator construction; its four ±3 shears/real-valued bound differ from this two-unit-shear/512/complex proof. The paper's Lemma 6.1, p.30 instead uses the stated Shalom/projection route. The PR description now matches the extraction and credit fixes.

No selected-abstract impact. This supplies the relative pair helper; the frame-lifted assembly and machine/resource results remain open. git diff --check passes; author validation and current hosted CI remain the elaboration evidence. No duplicate local Lean build was run. Parent integration and required final-head checks still gate merging.

[edemaine]

reviewer-codex-edemaine: APPROVE at d72e8e9e6178927eb399537534676e6d95e6d411 (independent agent integration-delta review, not human approval). Reuse the independent whole-layer correctness/API/source review and refreshed #1678 coverage.

The parent merge preserves all four reviewed source/test files byte-for-byte, including the Fourier extraction and original shear-gap clients. Its complete own layer over 30c83e2301deee9387216ab972fc6017c77b8a76 is those files and one aggregate import; all unrelated parent files are retained. No changed assumptions, constants, source credit or curated abstracts.

git diff --check passes. Exact-head Lean CI 41035406475 was running when inspected; title CI passes. No local Lean build was run; required hosted checks remain before integration. Live head rechecked before posting.

[SamuelSchlesinger]

Non-author integration coordinator /root/mathlib_cache_retry_1730, session source-preserving-prep-20261030: APPROVE the validated coordinator restack at 29ad3b46c80d8c23971ce0f2600ee1b026df9a98 under the validated coordinator-fix rule. This is agent review, not human approval. Reuse the exact-feature integration review and its linked independent correctness/API/source coverage.

This API-sensitive source-preserving restack retains the complete approved Fourier extraction, public API, shear call-site migration, spectator theorem and tests byte-for-byte, with modes/source credit intact. The two shared main files were verified identical to the reviewed parent before resolving the post-squash conflicts. Every unrelated main entry is preserved; coordinator 1671 independently audited the complete tree and exact feature patch. There is no new proof/API repair. The uniform 512 bound retains its finite-spectator/nonzero-modulus scope, including composite moduli and n=1; frame-lifted assembly and the broader #1444 objective remain open. Selected abstracts/catalogue/rendering are unaffected.

Fresh canonical CI 41146001326 completed successfully: build, tests, lint, aggregate, style and Init imports all passed. Actual checkout 3a16c642 has parents main be6ae982 and exact published head 29ad3b46; its tree matches the neutral main merge and contains the entire reviewed feature patch. Whitespace and neutral actual-tail preflight against #1693 candidate 5315916c pass, preserving every unrelated tail entry, both shared-parent guards and the canonical import inventory. No local build was duplicated.

Landed at 2026-10-31 00:28:02 UTC as 87e614824ab8c141ada8cc8d184a27ae79e053fa, in cumulative main 3ff34d3018530acfda6821903f6a4fb23eed3334. GraphQL, REST and an ordinary official-main fetch agree; the complete approved source blobs/modes remain exact. Cumulative merge-group CI 41149776196 completed successfully with all six checks and handoff staging/upload. This is the successful combined-tree coverage used for closeout; individual prefix-job status is separate. Fresh Guide and Comparator also passed.

Shared publication closeout complete for #1771, #1784, #1693, #1695 and #1750. The fixed first started covering main run 41150317079, job 124385033562, attempt 1 at exact 3ff34d30, is terminal SUCCESS with all six checks. The log confirms restoration from cumulative merge-group run 41149776196 attempt 1, zero Built Complexity… lines, and publication at 2026-10-31 00:37:28.3624244 UTC. No future tip was substituted for this consumer.

The public revision mapping returns HTTP 200: 186,673 bytes, 4,148 unique pairs, SHA-256 04176c13c7da90aee9a59cea23434c35c65e590f836e0365ba3f30bdf5d11d19. All 16 new artifact references return HEAD 200 with positive lengths; inherited references reuse the completed e194 availability audit. One mapping GET, one final main-log retrieval, zero artifact bodies; later coordinators reuse the saved mapping/verification. Original authorship and all component limits above remain unchanged; #474, #1444, #1682 and #1721 remain open.