feat(Expander): uniform spectral gap for the shear-translation graph on ZMod n × ZMod n

Complexity.lean

@@ -2364,8 +2364,10 @@ public import Complexity.Crypto.Protocols.SigmaProtocol.SchnorrSignature
 public import Complexity.Crypto.Protocols.Signature.RandomOracle
 public import Complexity.Foundations.Algebra.FiniteMagnitude
 public import Complexity.Foundations.Algebra.GeometricTail
+public import Complexity.Foundations.Algebra.Shear
 public import Complexity.Foundations.Analysis.Asymptotics.Exponential
 public import Complexity.Foundations.Analysis.BernoulliInequality
+public import Complexity.Foundations.Analysis.Fourier.ZModProd
 public import Complexity.Foundations.Analysis.HarmonicMean
 public import Complexity.Foundations.Analysis.InnerProductSpace.Basic
 public import Complexity.Foundations.Analysis.LpNorm
@@ -2467,6 +2469,7 @@ public import Complexity.Foundations.Combinatorics.Expander.Random
 public import Complexity.Foundations.Combinatorics.Expander.Reindex
 public import Complexity.Foundations.Combinatorics.Expander.Reingold
 public import Complexity.Foundations.Combinatorics.Expander.Replacement
+public import Complexity.Foundations.Combinatorics.Expander.ShearTranslation
 public import Complexity.Foundations.Combinatorics.Expander.SimpleGraph
 public import Complexity.Foundations.Combinatorics.Expander.SlotGraph
 public import Complexity.Foundations.Combinatorics.Expander.Spectrum

Complexity/Foundations/Algebra/Shear.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.Algebra.Group.End
+public import Mathlib.Algebra.Ring.Defs
+import Mathlib.Tactic.Ring
+
+/-!
+# Shears of `R × R`
+
+The shears `(x, y) ↦ (x + k * y, y)` and `(x, y) ↦ (x, y + k * x)` of `R × R` over a commutative
+ring, as permutations. The inverse of a shear is the opposite shear, and iterating a shear `m`
+times multiplies its parameter by `m`.
+
+## Main definitions
+
+* `Cslib.shearFst`, `Cslib.shearSnd`: the shears `(x, y) ↦ (x + k * y, y)` and
+  `(x, y) ↦ (x, y + k * x)` of `R × R`.
+
+## Main results
+
+* `Cslib.shearFst_symm`, `Cslib.shearSnd_symm`: the inverse of a shear is the opposite shear.
+* `Cslib.shearFst_pow`, `Cslib.shearSnd_pow`: iterating a shear `m` times multiplies its
+  parameter by `m`.
+-/
+
+@[expose] public section
+
+namespace Cslib
+
+variable {R : Type*} [CommRing R]
+
+/-- The shear `(x, y) ↦ (x + k * y, y)` of `R × R`, as a permutation. -/
+def shearFst (k : R) : Equiv.Perm (R × R) where
+  toFun v := (v.1 + k * v.2, v.2)
+  invFun v := (v.1 - k * v.2, v.2)
+  left_inv v := by simp
+  right_inv v := by simp
+
+/-- The shear `(x, y) ↦ (x, y + k * x)` of `R × R`, as a permutation. -/
+def shearSnd (k : R) : Equiv.Perm (R × R) where
+  toFun v := (v.1, v.2 + k * v.1)
+  invFun v := (v.1, v.2 - k * v.1)
+  left_inv v := by simp
+  right_inv v := by simp
+
+@[simp]
+theorem shearFst_apply (k : R) (v : R × R) : shearFst k v = (v.1 + k * v.2, v.2) :=
+  rfl
+
+@[simp]
+theorem shearSnd_apply (k : R) (v : R × R) : shearSnd k v = (v.1, v.2 + k * v.1) :=
+  rfl
+
+/-- The inverse of a shear is the opposite shear. -/
+theorem shearFst_symm (k : R) : (shearFst k).symm = shearFst (-k) := by
+  ext v <;> simp [shearFst, sub_eq_add_neg]
+
+/-- The inverse of a shear is the opposite shear. -/
+theorem shearSnd_symm (k : R) : (shearSnd k).symm = shearSnd (-k) := by
+  ext v <;> simp [shearSnd, sub_eq_add_neg]
+
+/-- Iterating a shear multiplies its parameter. -/
+theorem shearFst_pow (k : R) (m : ℕ) : shearFst k ^ m = shearFst (m * k) := by
+  induction m with
+  | zero => ext v <;> simp
+  | succ m ih =>
+    rw [pow_succ', ih]
+    ext v
+    · simp only [Equiv.Perm.mul_apply, shearFst_apply]
+      push_cast
+      ring
+    · rfl
+
+/-- Iterating a shear multiplies its parameter. -/
+theorem shearSnd_pow (k : R) (m : ℕ) : shearSnd k ^ m = shearSnd (m * k) := by
+  induction m with
+  | zero => ext v <;> simp
+  | succ m ih =>
+    rw [pow_succ', ih]
+    ext v
+    · rfl
+    · simp only [Equiv.Perm.mul_apply, shearSnd_apply]
+      push_cast
+      ring
+
+end Cslib

Complexity/Foundations/Analysis/Fourier/ZModProd.lean

@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
+import Complexity.Foundations.Algebra.Shear
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.NumberTheory.LegendreSymbol.AddCharacter
+
+/-!
+# The discrete Fourier transform on `ZMod N × ZMod N`
+
+The Fourier transform of `f : ZMod N × ZMod N → ℂ` at the frequency `ξ` is
+`∑ v, e (-(ξ.1 * v.1 + ξ.2 * v.2)) * f v`, where `e = ZMod.stdAddChar` sends `j` to
+`exp (2 π i j / N)`. This is Mathlib's `ZMod.dft` in each coordinate, written for the two
+coordinates together. The characters `v ↦ e (ξ.1 * v.1 + ξ.2 * v.2)` are orthogonal, so the
+transform preserves the `ℓ²` norm up to the factor `N ^ 2` (Parseval's identity).
+
+Translations and shears of the plane act on the transform by simple rules: a translation by `t`
+multiplies the transform at `ξ` by `e (ξ.1 * t.1 + ξ.2 * t.2)`, and the shear
+`(x, y) ↦ (x + k * y, y)` acts on the frequencies by the transposed inverse shear
+`(a, b) ↦ (a, b - k * a)`, and symmetrically for `(x, y) ↦ (x, y + k * x)`.
+
+## Main definitions
+
+* `ZMod.dftProd`: the discrete Fourier transform on `ZMod N × ZMod N`.
+
+## Main results
+
+* `ZMod.sum_norm_sq_dftProd`: Parseval's identity
+  `∑ ξ, ‖dftProd f ξ‖ ^ 2 = N ^ 2 * ∑ v, ‖f v‖ ^ 2`.
+* `ZMod.dftProd_zero`: the transform at the zero frequency is the sum of the values.
+* `ZMod.dftProd_comp_add`: translation multiplies the transform by a character value.
+* `ZMod.dftProd_comp_shearFst`, `ZMod.dftProd_comp_shearSnd`: shears permute the frequencies.
+-/
+
+public section
+
+namespace ZMod
+
+open Finset ComplexConjugate
+
+variable {N : ℕ} [NeZero N]
+
+/-- The discrete Fourier transform of `f : ZMod N × ZMod N → ℂ` at the frequency `ξ`:
+`∑ v, e (-(ξ.1 * v.1 + ξ.2 * v.2)) * f v` with `e = ZMod.stdAddChar`. -/
+noncomputable def dftProd (f : ZMod N × ZMod N → ℂ) (ξ : ZMod N × ZMod N) : ℂ :=
+  ∑ v, stdAddChar (-(ξ.1 * v.1 + ξ.2 * v.2)) * f v
+
+/-- The transform at the zero frequency is the sum of the values. -/
+@[simp]
+theorem dftProd_zero (f : ZMod N × ZMod N → ℂ) : dftProd f 0 = ∑ v, f v := by
+  simp [dftProd]
+
+/-- The transform is additive. -/
+theorem dftProd_sub (f g : ZMod N × ZMod N → ℂ) :
+    dftProd (f - g) = dftProd f - dftProd g := by
+  ext ξ
+  simp only [dftProd, Pi.sub_apply, mul_sub, sum_sub_distrib]
+
+/-- **Orthogonality of the characters of `ZMod N × ZMod N`**: summed over all frequencies, a
+nontrivial character value vanishes. -/
+private theorem sum_stdAddChar_mul_add (u : ZMod N × ZMod N) :
+    ∑ ξ : ZMod N × ZMod N, stdAddChar (ξ.1 * u.1 + ξ.2 * u.2) =
+      if u = 0 then (N : ℂ) ^ 2 else 0 := by
+  simp only [AddChar.map_add_eq_mul, Fintype.sum_prod_type, ← mul_sum, ← sum_mul,
+    AddChar.sum_mulShift _ (isPrimitive_stdAddChar N), ZMod.card]
+  rcases u with ⟨u₁, u₂⟩
+  by_cases h₁ : u₁ = 0 <;> by_cases h₂ : u₂ = 0 <;> simp [h₁, h₂, sq]
+
+/-- **Parseval's identity** on `ZMod N × ZMod N`. -/
+theorem sum_norm_sq_dftProd (f : ZMod N × ZMod N → ℂ) :
+    ∑ ξ, ‖dftProd f ξ‖ ^ 2 = N ^ 2 * ∑ v, ‖f v‖ ^ 2 := by
+  apply Complex.ofReal_injective
+  push_cast
+  simp only [← Complex.mul_conj', dftProd, map_sum, map_mul, ← AddChar.map_neg_eq_conj, neg_neg,
+    sum_mul_sum]
+  calc ∑ ξ : ZMod N × ZMod N, ∑ v, ∑ w,
+        stdAddChar (-(ξ.1 * v.1 + ξ.2 * v.2)) * f v * (stdAddChar (ξ.1 * w.1 + ξ.2 * w.2) *
+          conj (f w))
+      = ∑ v, ∑ w, f v * conj (f w) *
+          ∑ ξ : ZMod N × ZMod N, stdAddChar (ξ.1 * (w - v).1 + ξ.2 * (w - v).2) := by
+        rw [sum_comm]
+        refine sum_congr rfl fun v _ ↦ ?_
+        rw [sum_comm]
+        refine sum_congr rfl fun w _ ↦ ?_
+        rw [mul_sum]
+        refine sum_congr rfl fun ξ _ ↦ ?_
+        have : stdAddChar (ξ.1 * (w - v).1 + ξ.2 * (w - v).2) =
+            stdAddChar (-(ξ.1 * v.1 + ξ.2 * v.2)) * stdAddChar (ξ.1 * w.1 + ξ.2 * w.2) := by
+          rw [← AddChar.map_add_eq_mul]
+          congr 1
+          simp only [Prod.fst_sub, Prod.snd_sub]
+          ring
+        rw [this]
+        ring
+    _ = (N : ℂ) ^ 2 * ∑ v, f v * conj (f v) := by
+        simp only [sum_stdAddChar_mul_add, sub_eq_zero, mul_ite, mul_zero, sum_ite_eq',
+          mem_univ, ite_true, mul_sum]
+        exact sum_congr rfl fun v _ ↦ by ring
+
+/-- **Translation** multiplies the transform at `ξ` by `e (ξ.1 * t.1 + ξ.2 * t.2)`. -/
+theorem dftProd_comp_add (f : ZMod N × ZMod N → ℂ) (t ξ : ZMod N × ZMod N) :
+    dftProd (fun v ↦ f (v + t)) ξ = stdAddChar (ξ.1 * t.1 + ξ.2 * t.2) * dftProd f ξ := by
+  rw [dftProd, dftProd, mul_sum]
+  refine Fintype.sum_equiv (Equiv.addRight t) _ _ fun v ↦ ?_
+  simp only [Equiv.coe_addRight, Prod.fst_add, Prod.snd_add, ← mul_assoc,
+    ← AddChar.map_add_eq_mul]
+  congr 2
+  ring
+
+/-- **The shear `(x, y) ↦ (x + k * y, y)`** acts on frequencies by `(a, b) ↦ (a, b - k * a)`. -/
+theorem dftProd_comp_shearFst (f : ZMod N × ZMod N → ℂ) (k : ZMod N) (ξ : ZMod N × ZMod N) :
+    dftProd (fun v ↦ f (v.1 + k * v.2, v.2)) ξ = dftProd f (ξ.1, ξ.2 - k * ξ.1) := by
+  rw [dftProd, dftProd]
+  refine Fintype.sum_equiv (Cslib.shearFst k) _ _ fun v ↦ ?_
+  rw [Cslib.shearFst_apply]
+  congr 2
+  ring
+
+/-- **The shear `(x, y) ↦ (x, y + k * x)`** acts on frequencies by `(a, b) ↦ (a - k * b, b)`. -/
+theorem dftProd_comp_shearSnd (f : ZMod N × ZMod N → ℂ) (k : ZMod N) (ξ : ZMod N × ZMod N) :
+    dftProd (fun v ↦ f (v.1, v.2 + k * v.1)) ξ = dftProd f (ξ.1 - k * ξ.2, ξ.2) := by
+  rw [dftProd, dftProd]
+  refine Fintype.sum_equiv (Cslib.shearSnd k) _ _ fun v ↦ ?_
+  rw [Cslib.shearSnd_apply]
+  congr 2
+  ring
+
+end ZMod

Complexity/Foundations/Combinatorics/Expander/Perm.lean

@@ -41,6 +41,10 @@ are expanders [Hoory, Linial and Wigderson, Theorem 4.16][HooryLinialWigderson20
   permutations move out of it, twice.
 * `Cslib.RotationMap.le_edgeExpansion_ofPerms`: a lower bound on these counts for every set of at
   most half of the vertices bounds the edge expansion.
+* `Cslib.RotationMap.expect_mul_walk_ofPerms`: the Dirichlet form of the walk is the total squared
+  change of a function along the permutations.
+* `Cslib.RotationMap.secondEigenvalue_ofPerms_le`: a Poincaré inequality for the permutations
+  bounds the second eigenvalue.
 
 ## References
 
@@ -133,4 +137,63 @@ theorem le_edgeExpansion_ofPerms [Nontrivial V] {c : ℝ}
   push_cast at this ⊢
   linarith
 
+omit [DecidableEq V] in
+/-- **The Dirichlet form of a permutation multigraph**: the correlation of `f` with its walk is
+`𝔼 f²` minus `1 / (2 |K|)` times the total squared change `∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2` of `f`
+along the permutations. -/
+theorem expect_mul_walk_ofPerms [Nonempty K] (f : V → ℝ) :
+    𝔼 v, f v * (ofPerms σ).walk f v =
+      (𝔼 v, f v ^ 2) - (∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2) / (2 * Fintype.card K) := by
+  have hK : (0 : ℝ) < Fintype.card K := Nat.cast_pos.2 Fintype.card_pos
+  have hwalk (v : V) : (ofPerms σ).walk f v =
+      (∑ k, (f (σ k v) + f ((σ k).symm v))) / (2 * Fintype.card K) := by
+    rw [walk_apply, Fintype.expect_eq_sum_div_card, Fintype.sum_prod_type, Fintype.card_prod,
+      Fintype.card_bool]
+    simp only [Fintype.sum_bool, neighbor_ofPerms_true, neighbor_ofPerms_false,
+      add_comm (f ((σ _).symm v))]
+    push_cast
+    ring
+  have hsymm (k : K) : ∑ v, f v * f ((σ k).symm v) = ∑ v, f v * f (σ k v) := by
+    rw [← Equiv.sum_comp (σ k)]
+    simp [mul_comm]
+  have hcross (k : K) : ∑ v, (f (σ k v) - f v) ^ 2 =
+      2 * ∑ v, f v ^ 2 - 2 * ∑ v, f v * f (σ k v) := by
+    simp only [sub_sq, sum_add_distrib, sum_sub_distrib, Equiv.sum_comp (σ k) (fun v ↦ f v ^ 2),
+      mul_sum]
+    ring_nf
+    simp only [← sum_mul, mul_comm (f _) (f _)]
+  calc 𝔼 v, f v * (ofPerms σ).walk f v
+      = (∑ v, f v * ∑ k, (f (σ k v) + f ((σ k).symm v))) / (2 * Fintype.card K) /
+          Fintype.card V := by
+        simp only [hwalk, Fintype.expect_eq_sum_div_card, ← mul_div_assoc, ← sum_div]
+    _ = (2 * ∑ k, ∑ v, f v * f (σ k v)) / (2 * Fintype.card K) / Fintype.card V := by
+        congr 2
+        simp only [mul_sum, mul_add, sum_add_distrib]
+        rw [sum_comm, sum_comm (f := fun v k ↦ f v * f ((σ k).symm v))]
+        simp only [hsymm, ← two_mul, mul_sum]
+    _ = _ := by
+        simp only [Fintype.expect_eq_sum_div_card, ← sum_div, hcross, sum_sub_distrib, sum_const,
+          card_univ, nsmul_eq_mul, ← mul_sum]
+        field_simp
+        ring
+
+omit [DecidableEq V] in
+/-- **A Poincaré inequality bounds the second eigenvalue** of a permutation multigraph on at least
+two vertices: if `c 𝔼 f² ≤ ∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2` for every `f` of expectation zero, then
+`λ₂ ≤ 1 - c / (2 |K|)`. -/
+theorem secondEigenvalue_ofPerms_le [Nonempty K] [Nontrivial V] {c : ℝ}
+    (h : ∀ f : V → ℝ, 𝔼 v, f v = 0 → c * (𝔼 v, f v ^ 2) ≤ ∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2) :
+    (ofPerms σ).secondEigenvalue ≤ 1 - c / (2 * Fintype.card K) := by
+  refine (ofPerms σ).secondEigenvalue_le_iff.2 fun f hf ↦ ?_
+  have hK : (0 : ℝ) < 2 * Fintype.card K := by
+    have := Fintype.card_pos (α := K)
+    positivity
+  calc 𝔼 v, f v * (ofPerms σ).walk f v
+      = (𝔼 v, f v ^ 2) - (∑ k, 𝔼 v, (f (σ k v) - f v) ^ 2) / (2 * Fintype.card K) :=
+        expect_mul_walk_ofPerms σ f
+    _ ≤ (𝔼 v, f v ^ 2) - c * (𝔼 v, f v ^ 2) / (2 * Fintype.card K) := by
+        have := div_le_div_of_nonneg_right (h f hf) hK.le
+        linarith
+    _ = (1 - c / (2 * Fintype.card K)) * 𝔼 v, f v ^ 2 := by ring
+
 end Cslib.RotationMap