Newman's theorem for Γ₀(N)

The primitive representative and local valuation argument is proved for arbitrary subgroups in NormalizerDelta/NewmanGen. Here it is instantiated with newmanData_gamma0, which supplies Γ₀(N)'s lattice, unipotents and valuation witnesses. The specialized local and final theorems are wrappers around that shared argument, with no inverse-representative hypothesis needed.

theorem CongruenceNormalizers.local_conclusion {N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat (hPart N) α β γ δ) (he : α * δ - β * γ ≠ 0) (hprim : ∀ (p : ℕ), Nat.Prime p → ¬(↑p ∣ α ∧ ↑p ∣ β ∧ ↑p ∣ γ ∧ ↑p ∣ δ)) {p : ℕ} (hp : Nat.Prime p) : have B := vz p (α * δ - β * γ) + N.factorization p + 1; vz p (α * δ - β * γ) = 0 ∧ (nPart N).factorization p ≤ vv B p γ ∨ vz p (α * δ - β * γ) = (nPart N).factorization p ∧ (nPart N).factorization p ≤ vv B p α ∧ (nPart N).factorization p ≤ vv B p γ ∧ (nPart N).factorization p ≤ vv B p δ

theorem CongruenceNormalizers.newman' {N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hg : g ∈ Norm0 N) : IsNewmanForm N g