{"id":"palomar/PALOMAR-2026-10-18-000023","url":"https://github.com/F-Najman/normalizer-lean/tree/17c911351938f13d620262a54de45c275db9de57","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000023-v2.json","repo":"https://github.com/F-Najman/normalizer-lean","tags":["math.NT","math.GR","msc:11F06","msc:20H05","msc:14G35","msc:14H37","msc:68V20","modular-forms","normalizers","lean"],"score":0,"title":"Normalizers of Γ_Δ(N): the group M_Δ, finiteness, and a coset count","trust":"high","domain":"math.NT","source":"palomar","authors":["Filip Najman"],"reviews":0,"subject":"math.NT","summary":"Formal statements and proofs, in Lean 4 with Mathlib, about the normalizers in SL₂(ℝ) of the groups Γ_Δ(N) between Γ₁(N) and Γ₀(N), and the quotients Nor(Γ_Δ(N))/Γ_Δ(N), which for −1 ∈ Δ are the modular automorphism groups of the curves X_Δ(N): the matrices allowed by the generalized Newman bound h_Δ form a group M_Δ = D⁻¹Γ₀(n_Δ)⁺D, D = diag(h_Δ, 1), which contains Nor(Γ_Δ(N)) and contains Γ₀(N) with finite index, so Nor(Γ_Δ(N))/Γ_Δ(N) is finite for every Δ; its order is [(ℤ/N)ˣ : Δ] times the number of pairs (σ, H), with σ in a fixed set of representatives of Γ₀(N)\\SL₂(ℤ) and H a Hermite…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true}