Newman's theorem, step 2 continued: the integer divisibilities

For g = κ·S ∈ Norm(Γ₀(N)), S = [[α, β/h], [hγ, δ]], e = αδ − βγ, with h = h(N), n = n(N), ε = gcd(N, 24):

• F1 e ∣ h·αγ F2 e ∣ α² F3 eN ∣ h²γ² F4 eε ∣ 2h·αγ
• F5 e ∣ nh·βδ F6 e ∣ n·β² F7 e ∣ δ² F8 eε ∣ 2nh·βδ
• F9 e ∣ N·βγ F10 eh ∣ N·αβ F11 eN ∣ Nh·γδ F12 eε ∣ 2N·βγ
• and, for [[x, y], [N, t]] ∈ Γ₀(N) and s = t − x, the same four with s in place of N.

theorem CongruenceNormalizers.newmanData_gamma0 (N : ℕ) : NewmanData N (Gamma0R N) (epsPart N) (hPart N)

The generic Newman hypotheses for Γ₀(N).

theorem CongruenceNormalizers.InL.entries {N : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) : ∃ (a : ℤ) (b : ℤ) (c : ℤ) (d : ℤ), M 0 0 = ↑a ∧ M 0 1 = ↑b ∧ M 1 0 = ↑c ∧ M 1 1 = ↑d ∧ ↑N ∣ c ∧ ↑(epsPart N) ∣ d - a

theorem CongruenceNormalizers.phi_InL {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat (hPart N) α β γ δ) {Y : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hY : Y ∈ Gamma0R N) : InL N (Phi (hPart N) α β γ δ ↑Y)

theorem CongruenceNormalizers.InL.nsmul' {N : ℕ} {M : Matrix (Fin 2) (Fin 2) ℝ} (h : InL N M) (m : ℕ) : InL N (↑m • M)

theorem CongruenceNormalizers.InL_basic {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat (hPart N) α β γ δ) (he : α * δ - β * γ ≠ 0) : InL N (Phi (hPart N) α β γ δ !![0, 1; 0, 0]) ∧ InL N (↑N • Phi (hPart N) α β γ δ !![0, 0; 1, 0]) ∧ InL N (↑N • Phi (hPart N) α β γ δ !![0, 0; 0, 1])

theorem CongruenceNormalizers.InL_s {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat (hPart N) α β γ δ) (he : α * δ - β * γ ≠ 0) {x y t : ℤ} (hdet : x * t - y * ↑N = 1) : InL N (↑(t - x) • Phi (hPart N) α β γ δ !![0, 0; 0, 1]) ∧ ↑(epsPart N) ∣ t - x

theorem CongruenceNormalizers.int_facts {N : ℕ} [NeZero N] {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat (hPart N) α β γ δ) (he : α * δ - β * γ ≠ 0) : α * δ - β * γ ∣ ↑(hPart N) * (α * γ) ∧ α * δ - β * γ ∣ 1 * α ^ 2 ∧ (α * δ - β * γ) * ↑N ∣ ↑(hPart N) ^ 2 * γ ^ 2 ∧ (α * δ - β * γ) * ↑(epsPart N) ∣ 2 * ↑(hPart N) * (α * γ) ∧ α * δ - β * γ ∣ ↑(nPart N) * ↑(hPart N) * (β * δ) ∧ α * δ - β * γ ∣ ↑(nPart N) * β ^ 2 ∧ α * δ - β * γ ∣ 1 * δ ^ 2 ∧ (α * δ - β * γ) * ↑(epsPart N) ∣ 2 * ↑(nPart N) * ↑(hPart N) * (β * δ) ∧ α * δ - β * γ ∣ ↑N * (β * γ) ∧ (α * δ - β * γ) * ↑(hPart N) ∣ ↑N * (α * β) ∧ (α * δ - β * γ) * ↑N ∣ ↑N * ↑(hPart N) * (γ * δ) ∧ (α * δ - β * γ) * ↑(epsPart N) ∣ 2 * ↑N * (β * γ)

theorem CongruenceNormalizers.int_facts_s {N : ℕ} {g : Matrix.SpecialLinearGroup (Fin 2) ℝ} (hgN : g ∈ Norm0 N) {κ : ℝ} {α β γ δ : ℤ} (hg : ↑g = κ • Smat (hPart N) α β γ δ) (he : α * δ - β * γ ≠ 0) {x y t : ℤ} (hdet : x * t - y * ↑N = 1) : α * δ - β * γ ∣ (t - x) * (β * γ) ∧ (α * δ - β * γ) * ↑(hPart N) ∣ (t - x) * (α * β) ∧ (α * δ - β * γ) * ↑N ∣ (t - x) * ↑(hPart N) * (γ * δ) ∧ (α * δ - β * γ) * ↑(epsPart N) ∣ 2 * (t - x) * (β * γ)