{"id":"palomar/PALOMAR-2026-10-18-000012","url":"https://github.com/F-Najman/normalizer-lean/tree/e7ca694d9e349326e03e5acfa4e41ed823e4e2dc","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000012-v2.json","repo":"https://github.com/F-Najman/normalizer-lean","tags":["math.NT","math.GR","msc:11F06","msc:20H05","msc:20F05","msc:68V20","modular-curves","normalizers","lean","group-presentations"],"score":0,"title":"The normalizer of Γ₀(N): Newman's theorem, and the order and presentations of B(N)","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 B(N) = Nor(Γ₀(N))/Γ₀(N), the normalizer of Γ₀(N) in SL₂(ℝ) modulo Γ₀(N), for every N ≥ 1: Newman's theorem describing the normalizer, in both directions; the order |B(N)| = 2^ω(n) ψ(N)/ψ(n), where h is the largest divisor of 24 with h² ∣ N and n = N/h²; generators and complete presentations of B(N) for every N; a criterion for B(N) to be the internal direct product of its local factors; B(18) ≅ S₄; and the errors in the published presentations: the Akbaş–Singerman relation fails in B(256), and Bars's presentations at levels 32, 64…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-20","reactions":{},"formalized":true}