Import Newman normalizer bounds for congruence subgroups

LeanPool/CongruenceNormalizers.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2026 Filip Najman. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Filip Najman
+-/
+
+module
+
+public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanMain
+public import LeanPool.CongruenceNormalizers.NormalizerDelta.NewmanDelta
+
+/-!
+# Newman normalizer bounds for congruence subgroups
+
+Source: doi:10.1017/S001708950000940X, url:https://github.com/F-Najman/normalizer-lean/tree/ea4445c0d991a65d54fc77af0af559f2322e8660
+Authors: Filip Najman
+Status: verified
+Main declarations: `CongruenceNormalizers.newman_iff`, `CongruenceNormalizers.newman_delta`
+Tags: modular-forms, congruence-subgroups, normalizers, arithmetic-groups
+MSC: 11F06, 20H05
+-/
+
+/-
+Adapted from Filip Najman's Apache-2.0 `normalizer-lean`, commit
+`ea4445c0d991a65d54fc77af0af559f2322e8660`. The upstream proofs were written by
+Claude Code agents following the author's mathematical blueprints.
+-/
+
+public section
+
+namespace CongruenceNormalizers
+
+open Matrix MatrixGroups
+
+/-- Newman's integral matrix form characterizes the real normalizer of Γ₀(N). -/
+theorem newman_iff {N : ℕ} [NeZero N] {g : SL(2, ℝ)} :
+    g ∈ Norm0 N ↔ IsNewmanForm N g :=
+  ⟨newman', newmanForm_mem_normalizer'⟩
+
+/-- The corresponding necessary matrix form for the normalizer of Γ_Δ(N). -/
+theorem newman_delta {N : ℕ} [NeZero N] (Δ : Subgroup (ZMod N)ˣ)
+    {g : SL(2, ℝ)} (hg : g ∈ NormG (GammaDeltaR N Δ)) :
+    IsNewmanFormH N (hDelta N Δ) g :=
+  newman_delta' Δ hg
+
+end CongruenceNormalizers

LeanPool/CongruenceNormalizers/Imports.lean

@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module  -- shake: keep-all --deprecated_module: ignore
+
+-- Generated project imports; run `lake exe mk_all`.
+public import LeanPool.CongruenceNormalizers
+public import LeanPool.CongruenceNormalizers.NormalizerDelta.Basic
+public import LeanPool.CongruenceNormalizers.NormalizerDelta.Defs
+public import LeanPool.CongruenceNormalizers.NormalizerDelta.NewmanDelta
+public import LeanPool.CongruenceNormalizers.NormalizerDelta.NewmanGen
+public import LeanPool.CongruenceNormalizers.NormalizerLean.AtkinLehner
+public import LeanPool.CongruenceNormalizers.NormalizerLean.Basic
+public import LeanPool.CongruenceNormalizers.NormalizerLean.Defs
+public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanCond
+public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanFacts
+public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanMain
+public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanRat
+public import LeanPool.CongruenceNormalizers.NormalizerLean.NewmanVal
+public import LeanPool.CongruenceNormalizers.NormalizerLean.T1General

LeanPool/CongruenceNormalizers/NormalizerDelta/Basic.lean

@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2026 Filip Najman. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Filip Najman
+-/
+module
+
+public import LeanPool.CongruenceNormalizers.NormalizerDelta.NewmanGen
+
+/-!
+# Γ_Δ(N), ε_Δ, h_Δ: basic facts
+
+* membership in Γ_Δ(N) and its image in SL₂(ℝ); T, U ∈ Γ_Δ(N);
+* ε_Δ ∣ N and ε_Δ ∣ d² − 1 for d ∈ Δ (`dvd_epsDelta_iff`), hence every element of Γ_Δ(N) lies in the
+  lattice L_{ε_Δ} (`inLe_of_mem_GammaDeltaR`);
+* v_p(h_Δ) = min(v_p(ε_Δ), ⌊v_p(N)/2⌋) (`factorization_hDelta`);
+* the element γ_p ∈ Γ_Δ(N) (`exists_gamma_delta`): if v_p(ε_Δ) < v_p(N), some d ∈ Δ has
+  v_p(d² − 1) = v_p(ε_Δ), and [[x, y], [N, d]] has v_p(d − x) = v_p(ε_Δ).
+-/
+
+@[expose] public section
+
+open Matrix MatrixGroups
+
+namespace CongruenceNormalizers
+
+noncomputable section
+
+variable {N : ℕ} {Δ : Subgroup (ZMod N)ˣ}
+
+theorem mem_toR {Γ : Subgroup SL(2, ℤ)} {g : SL(2, ℝ)} : g ∈ toR Γ ↔ ∃ γ ∈ Γ, ofZ γ = g :=
+  Subgroup.mem_map
+
+theorem ofZ_mem_toR {Γ : Subgroup SL(2, ℤ)} {γ : SL(2, ℤ)} (h : γ ∈ Γ) : ofZ γ ∈ toR Γ :=
+  Subgroup.mem_map_of_mem _ h
+
+theorem coe_ofZ (γ : SL(2, ℤ)) :
+    (ofZ γ : Matrix (Fin 2) (Fin 2) ℝ) = !![(γ 0 0 : ℝ), γ 0 1; γ 1 0, γ 1 1] := by
+  ext i j; fin_cases i <;> fin_cases j <;> rfl
+
+theorem GammaDelta_le_Gamma0 : GammaDelta N Δ ≤ CongruenceSubgroup.Gamma0 N := fun _ h => h.1
+
+theorem GammaDeltaR_le_Gamma0R : GammaDeltaR N Δ ≤ Gamma0R N :=
+  Subgroup.map_mono GammaDelta_le_Gamma0
+
+/-- An integer matrix of determinant 1. -/
+def mkSL (a b c d : ℤ) (h : a * d - b * c = 1) : SL(2, ℤ) := ⟨!![a, b; c, d], by
+  rw [det_fin_two_of]; exact h⟩
+
+theorem mkSL_mem_GammaDelta {a b c d : ℤ} (h : a * d - b * c = 1) (hc : (N : ℤ) ∣ c)
+    {u : (ZMod N)ˣ} (hu : u ∈ Δ) (hud : (u : ZMod N) = (d : ZMod N)) :
+    mkSL a b c d h ∈ GammaDelta N Δ := by
+  refine ⟨?_, u, hu, by simpa [mkSL] using hud⟩
+  rw [CongruenceSubgroup.Gamma0_mem]
+  simpa [mkSL] using (ZMod.intCast_zmod_eq_zero_iff_dvd c N).2 hc
+
+theorem coe_ofZ_mkSL {a b c d : ℤ} (h : a * d - b * c = 1) :
+    (ofZ (mkSL a b c d h) : Matrix (Fin 2) (Fin 2) ℝ) = !![(a : ℝ), b; c, d] := by
+  rw [coe_ofZ]; rfl
+
+theorem matT_mem_GammaDeltaR : matT ∈ GammaDeltaR N Δ := by
+  have h : (1 : ℤ) * 1 - 1 * 0 = 1 := by norm_num
+  refine mem_toR.2 ⟨mkSL 1 1 0 1 h, mkSL_mem_GammaDelta h (dvd_zero _) (Subgroup.one_mem _)
+    (by simp), ?_⟩
+  apply Subtype.ext
+  rw [coe_ofZ_mkSL]
+  simp [matT]
+
+theorem matU_mem_GammaDeltaR : matU N ∈ GammaDeltaR N Δ := by
+  have h : (1 : ℤ) * 1 - 0 * N = 1 := by norm_num
+  refine mem_toR.2 ⟨mkSL 1 0 N 1 h, mkSL_mem_GammaDelta h (dvd_refl _) (Subgroup.one_mem _)
+    (by simp), ?_⟩
+  apply Subtype.ext
+  rw [coe_ofZ_mkSL]
+  simp [matU]
+
+/-! ### ε_Δ -/
+
+theorem dvd_epsDelta_iff [NeZero N] {m : ℕ} :
+    m ∣ epsDelta N Δ ↔ m ∣ N ∧ ∀ u ∈ Δ, m ∣ (u : ZMod N).val ^ 2 - 1 := by
+  classical
+  unfold epsDelta
+  rw [Nat.dvd_gcd_iff, Finset.dvd_gcd_iff]
+  simp only [Finset.mem_filter, Finset.mem_univ, true_and]
+
+theorem epsDelta_dvd [NeZero N] : epsDelta N Δ ∣ N := (dvd_epsDelta_iff.1 dvd_rfl).1
+
+theorem epsDelta_dvd_val [NeZero N] {u : (ZMod N)ˣ} (hu : u ∈ Δ) :
+    epsDelta N Δ ∣ (u : ZMod N).val ^ 2 - 1 := (dvd_epsDelta_iff.1 dvd_rfl).2 u hu
+
+theorem epsDelta_pos [NeZero N] : 0 < epsDelta N Δ :=
+  Nat.pos_of_dvd_of_pos epsDelta_dvd (Nat.pos_of_ne_zero (NeZero.ne N))
+
+/-- For N ≥ 2 a unit has a positive representative. -/
+theorem one_le_val_unit (hN : 2 ≤ N) (u : (ZMod N)ˣ) : 1 ≤ (u : ZMod N).val := by
+  have : NeZero N := ⟨by omega⟩
+  have : Nontrivial (ZMod N) := ZMod.nontrivial_iff.2 (by omega)
+  by_contra h
+  have h0 : (u : ZMod N).val = 0 := by omega
+  rw [ZMod.val_eq_zero] at h0
+  exact u.ne_zero h0
+
+/-- The integer form of ε_Δ ∣ val(u)² − 1. -/
+theorem epsDelta_dvd_val_int [NeZero N] {u : (ZMod N)ˣ} (hu : u ∈ Δ) :
+    (epsDelta N Δ : ℤ) ∣ ((u : ZMod N).val : ℤ) ^ 2 - 1 := by
+  by_cases hN : N = 1
+  · have : epsDelta N Δ = 1 := Nat.dvd_one.1 (hN ▸ epsDelta_dvd)
+    rw [this]; exact one_dvd _
+  have h1 := one_le_val_unit (by have := NeZero.ne N; omega) u
+  have := Int.natCast_dvd_natCast.2 (epsDelta_dvd_val hu)
+  rwa [Nat.cast_sub (Nat.one_le_pow _ _ h1), Nat.cast_pow, Nat.cast_one] at this
+
+/-- Every element of Γ_Δ(N) lies in the lattice L_{ε_Δ}. -/
+theorem inLe_of_mem_GammaDeltaR [NeZero N] {Y : SL(2, ℝ)} (hY : Y ∈ GammaDeltaR N Δ) :
+    InLe N (epsDelta N Δ) (Y : Matrix (Fin 2) (Fin 2) ℝ) := by
+  obtain ⟨γ, ⟨h0, u, hu, hγ⟩, rfl⟩ := mem_toR.1 hY
+  refine ⟨γ 0 0, γ 0 1, γ 1 0, γ 1 1, coe_ofZ γ, ?_, ?_⟩
+  · exact (ZMod.intCast_zmod_eq_zero_iff_dvd _ N).1 (CongruenceSubgroup.Gamma0_mem.1 h0)
+  · have hc : (N : ℤ) ∣ γ 1 0 :=
+      (ZMod.intCast_zmod_eq_zero_iff_dvd _ N).1 (CongruenceSubgroup.Gamma0_mem.1 h0)
+    have hdet : γ 0 0 * γ 1 1 - γ 0 1 * γ 1 0 = 1 := by
+      have := γ.2; rwa [det_fin_two] at this
+    set v : ℤ := ((u : ZMod N).val : ℤ)
+    have hv : (N : ℤ) ∣ γ 1 1 - v := by
+      rw [← ZMod.intCast_eq_intCast_iff_dvd_sub]
+      simp only [v, Int.cast_natCast, ZMod.natCast_zmod_val]
+      exact hγ
+    have hεN : (epsDelta N Δ : ℤ) ∣ N := Int.natCast_dvd_natCast.2 epsDelta_dvd
+    obtain ⟨k1, hk1⟩ := hεN.trans hv
+    obtain ⟨k2, hk2⟩ := epsDelta_dvd_val_int hu
+    obtain ⟨k3, hk3⟩ := hεN.trans hc
+    refine ⟨-(γ 1 1 * (γ 0 1 * k3)) + γ 0 0 * ((γ 1 1 + v) * k1 + k2), ?_⟩
+    linear_combination -(γ 1 1) * hdet - (γ 1 1) * (γ 0 1) * hk3 + (γ 0 0) * (γ 1 1 + v) * hk1 +
+      (γ 0 0) * hk2
+
+/-! ### h_Δ -/
+
+theorem factorization_hDelta [NeZero N] (p : ℕ) :
+    (hDelta N Δ).factorization p =
+      min ((epsDelta N Δ).factorization p) (N.factorization p / 2) := by
+  unfold hDelta
+  rw [Nat.factorization_prod (fun q hq => pow_ne_zero _ (Nat.prime_of_mem_primeFactors hq).ne_zero),
+    Finset.sum_apply']
+  rw [Finset.sum_congr rfl (fun q hq => by
+    rw [(Nat.prime_of_mem_primeFactors hq).factorization_pow, Finsupp.single_apply]),
+    Finset.sum_ite_eq']
+  split_ifs with hp
+  · rfl
+  · have : N.factorization p = 0 := by
+      rwa [← Finsupp.notMem_support_iff, Nat.support_factorization]
+    simp [this]
+
+end
+
+end CongruenceNormalizers

LeanPool/CongruenceNormalizers/NormalizerDelta/Defs.lean

@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2026 Filip Najman. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Filip Najman
+-/
+module
+
+public import LeanPool.CongruenceNormalizers.NormalizerLean.Defs
+
+/-! The definitions of Part 2 are in `NormalizerLean/Defs.lean`, with those of all six parts.
+This file
+only imports them, so that `Statements.lean`, which imports this file, is unchanged since
+freezing. -/
+
+@[expose] public section

LeanPool/CongruenceNormalizers/NormalizerDelta/NewmanDelta.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2026 Filip Najman. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Filip Najman
+-/
+module
+
+public import LeanPool.CongruenceNormalizers.NormalizerDelta.Basic
+
+/-!
+# The generalized Newman bound (`newman_delta'`)
+
+Γ_Δ(N) satisfies the hypotheses `NewmanData N (Γ_Δ(N)) ε_Δ h_Δ` of the generic Newman argument
+(`NewmanGen.lean`); the only new ingredient is the element γ_p (`exists_gamma_delta`):
+if j = v_p(ε_Δ) < ν = v_p(N), then p^{j+1} ∣ N, so p^{j+1} ∤ d² − 1 for some d ∈ Δ (otherwise
+p^{j+1} ∣ ε_Δ), while p^j ∣ ε_Δ ∣ d² − 1.  With t = d and x t − y N = 1, the matrix
+[[x, y], [N, t]] lies in Γ_Δ(N), and t(t − x) ≡ t² − 1 (mod N) gives v_p(t − x) = j (`gamma_val`).
+-/
+
+@[expose] public section
+
+open Matrix MatrixGroups
+
+namespace CongruenceNormalizers
+
+noncomputable section
+
+variable {N : ℕ} {Δ : Subgroup (ZMod N)ˣ}
+
+/-- The element γ_p of Γ_Δ(N). -/
+theorem exists_gamma_delta [NeZero N] {p : ℕ} (hp : p.Prime) (hpN : p ∣ N)
+    (hj : (epsDelta N Δ).factorization p < N.factorization p) :
+    ∃ x y t : ℤ, x * t - y * N = 1 ∧
+      (∃ γ ∈ GammaDeltaR N Δ, (γ : Matrix (Fin 2) (Fin 2) ℝ) = !![(x : ℝ), y; N, t]) ∧
+      t - x ≠ 0 ∧ vz p (t - x) = (epsDelta N Δ).factorization p := by
+  have hN := NeZero.ne N
+  have hN2 : 2 ≤ N := le_trans hp.two_le (Nat.le_of_dvd (Nat.pos_of_ne_zero hN) hpN)
+  set j := (epsDelta N Δ).factorization p with hjdef
+  set ν := N.factorization p with hν
+  have hε0 : epsDelta N Δ ≠ 0 := epsDelta_pos.ne'
+  -- some u ∈ Δ with p^{j+1} ∤ val(u)² − 1
+  obtain ⟨u, hu, hnd⟩ : ∃ u ∈ Δ, ¬ p ^ (j + 1) ∣ (u : ZMod N).val ^ 2 - 1 := by
+    by_contra hcon
+    push Not at hcon
+    have h1 : p ^ (j + 1) ∣ N := (hp.pow_dvd_iff_le_factorization hN).2 (by omega)
+    have h2 : p ^ (j + 1) ∣ epsDelta N Δ := dvd_epsDelta_iff.2 ⟨h1, hcon⟩
+    have := (hp.pow_dvd_iff_le_factorization hε0).1 h2
+    omega
+  have hpj : p ^ j ∣ (u : ZMod N).val ^ 2 - 1 :=
+    (Nat.ordProj_dvd (epsDelta N Δ) p).trans (epsDelta_dvd_val hu)
+  set v := (u : ZMod N).val with hvdef
+  have hv1 : 1 ≤ v := one_le_val_unit hN2 u
+  have hcopN : Nat.Coprime v N := ZMod.val_coe_unit_coprime u
+  -- Bézout: x v − y N = 1
+  have hb := Int.gcd_eq_gcd_ab v N
+  rw [Int.gcd_natCast_natCast, hcopN] at hb
+  set x := Int.gcdA v N
+  set y := -Int.gcdB v N
+  have hdet : x * v - y * N = 1 := by
+    push_cast at hb
+    simp only [y]
+    linear_combination -hb
+  refine ⟨x, y, v, hdet, ?_, ?_⟩
+  · have hdet' : x * v - y * N = 1 := hdet
+    refine ⟨ofZ (mkSL x y N v hdet'), ofZ_mem_toR (mkSL_mem_GammaDelta hdet' (dvd_refl _) hu ?_),
+      coe_ofZ_mkSL hdet'⟩
+    simp [v]
+  · -- the valuation, by `gamma_val` with the roles of x and t exchanged
+    have hdet2 : (v : ℤ) * x - y * N = 1 := by linear_combination hdet
+    have hpν : (p : ℤ) ^ ν ∣ (N : ℤ) := by exact_mod_cast Nat.ordProj_dvd N p
+    have hpv : IsCoprime (p : ℤ) (v : ℤ) := by
+      rw [Int.isCoprime_iff_gcd_eq_one, Int.gcd_natCast_natCast]
+      exact (Nat.Coprime.coprime_dvd_right hpN hcopN).symm
+    have hcast : (((v ^ 2 - 1 : ℕ)) : ℤ) = (v : ℤ) ^ 2 - 1 := by
+      rw [Nat.cast_sub (Nat.one_le_pow _ _ hv1)]; push_cast; ring
+    have hρ1 : (p : ℤ) ^ j ∣ 1 - (v : ℤ) ^ 2 := by
+      have := Int.natCast_dvd_natCast.2 hpj
+      rw [hcast] at this
+      push_cast at this
+      have := this.neg_right
+      convert this using 1; ring
+    have hρ2 : ¬ (p : ℤ) ^ (j + 1) ∣ 1 - (v : ℤ) ^ 2 := by
+      intro hd
+      apply hnd
+      have hd' : (p : ℤ) ^ (j + 1) ∣ (((v ^ 2 - 1 : ℕ)) : ℤ) := by
+        rw [hcast]; have := hd.neg_right; convert this using 1; ring
+      exact_mod_cast hd'
+    rcases gamma_val hp hdet2 hpν (by simp) hpv hρ1 hρ2 with h | ⟨-, hne, hval⟩
+    · omega
+    · refine ⟨fun h0 => hne (by linear_combination -h0), ?_⟩
+      rw [show (v : ℤ) - x = -(x - v) by ring, vz_neg]
+      exact hval
+
+/-- Γ_Δ(N) satisfies the hypotheses of the generic Newman argument. -/
+theorem newmanData_delta (N : ℕ) [NeZero N] (Δ : Subgroup (ZMod N)ˣ) :
+    NewmanData N (GammaDeltaR N Δ) (epsDelta N Δ) (hDelta N Δ) where
+  le := GammaDeltaR_le_Gamma0R
+  T_mem := matT_mem_GammaDeltaR
+  U_mem := matU_mem_GammaDeltaR
+  inL := fun _ hY => inLe_of_mem_GammaDeltaR hY
+  eps_dvd := epsDelta_dvd
+  h_pos := by unfold hDelta; exact Finset.prod_pos (fun q hq => pow_pos
+    (Nat.pos_of_mem_primeFactors hq) _)
+  h_sq_dvd := by
+    have hN := NeZero.ne N
+    have hh : hDelta N Δ ≠ 0 := by
+      unfold hDelta
+      exact Finset.prod_ne_zero_iff.2 (fun q hq => pow_ne_zero _ (Nat.pos_of_mem_primeFactors
+        hq).ne')
+    rw [← Nat.factorization_le_iff_dvd (pow_ne_zero 2 hh) hN]
+    intro p
+    rw [Nat.factorization_pow, Finsupp.smul_apply, smul_eq_mul, factorization_hDelta]
+    omega
+  h_fact := factorization_hDelta
+  gamma := fun _ hp hpN hj => exists_gamma_delta hp hpN hj
+
+/-- **The generalized Newman bound.** -/
+theorem newman_delta' {N : ℕ} [NeZero N] (Δ : Subgroup (ZMod N)ˣ) {g : SL(2, ℝ)}
+    (hg : g ∈ NormG (GammaDeltaR N Δ)) : IsNewmanFormH N (hDelta N Δ) g :=
+  newmanG (newmanData_delta N Δ) hg
+
+end
+
+end CongruenceNormalizers