Rationality of j(τ₁₆₃): the three-prime argument (Phase C, §4.2)

This file implements PhaseC-PLAN.md §4.2, the "three-prime argument" proving that j₀ := j τ₁₆₃ is rational (hence, with statement 1, an integer).

The top-level target is

theorem j_τ₁₆₃_rational_of (hsurj : Function.Surjective (j : ℍ → ℂ))
    (hint : IsIntegral ℤ (j τ₁₆₃)) : ∃ r : ℚ, j τ₁₆₃ = (r : ℂ)

gated on surjectivity of j (proved in parallel in Valence.lean) and on integrality of j τ₁₆₃ (statement 1, proved in parallel).

Structure of the proof (steps (C1)–(C7) of the plan)

Let j₀ := j τ₁₆₃ and x an arbitrary complex root of minpoly ℚ j₀.

• (C1)/(C2, transport) Rather than a field embedding, we transport polynomial identities via minpoly.dvd: if Φ_m(j₀, j₀) = 0 then minpoly ℚ j₀ ∣ diagPhiQ Φ_m (the diagonal G_m(X) = Φ_m(X, X) ∈ ℚ[X]), so Φ_m(x, x) = G_m(x) = 0 for every root x.
• (C2, input) For each m ∈ {41, 43, 61} the CM matrix M_n = [[n+1,−41],[1,n]] (CMRelations.cmMatrix_fixes) fixes τ₁₆₃; decomposing M_n = γ · Acol m n with γ ∈ SL(2,ℤ) shows some coset value f m i τ₁₆₃ = j τ₁₆₃, whence G_m(j₀) = 0.
• (C3) Surjectivity gives τ′ with j τ′ = x.
• (C4) G_m(x) = 0 = ∏_i (x − f m i τ′) produces a coset coincidence f m i τ′ = j τ′, hence an integer matrix of determinant m fixing τ′, i.e. a positive-definite integer form of discriminant t² − 4m rooted at τ′.
• (C5) The three forms are integer multiples of the common primitive form of τ′ (discriminant D₀); FormReduction.disc_of_three_relations forces D₀ = −163.
• (C6) FormReduction.cm_disc_neg163_smul_eq_τ₁₆₃: τ′ is Γ-equivalent to τ₁₆₃.
• (C7) Hence x = j τ′ = j τ₁₆₃ = j₀; every root of minpoly ℚ j₀ equals j₀, and the Vieta relation on the subleading coefficient (a rational) forces j₀ ∈ ℚ.

(C1)/(C2) The diagonal polynomial G_m(X) = Φ_m(X, X) ∈ ℚ[X] and its evaluation

noncomputable def Chudnovsky.diagPhiQ (PhiQ : Polynomial (Polynomial ℚ)) : Polynomial ℚ

The diagonal polynomial G_m(X) := Φ_m(X, X) ∈ ℚ[X], obtained by substituting the outer variable X for the coefficient variable Y (the ℚ-analogue of diagPhiZ).

Equations

• Chudnovsky.diagPhiQ PhiQ = Polynomial.eval Polynomial.X PhiQ

theorem Chudnovsky.diagQ_aeval_eq (PhiQ : Polynomial (Polynomial ℚ)) (z : ℂ) : (Polynomial.aeval z) (diagPhiQ PhiQ) = Polynomial.eval z ((specializeY z) PhiQ)

The diagonal substitution commutes with Y ↦ z: G_m(z) = Φ_m(z, z) for z : ℂ, where the left side is aeval z (diagPhiQ Φ_m) and the right side is (specializeY z Φ_m).eval z.

theorem Chudnovsky.diagQ_eval_eq_prod {m : ℕ} [NeZero m] {PhiQ : Polynomial (Polynomial ℚ)} (hPhiQ : ∀ (τ : UpperHalfPlane), orbitPoly m τ = (specializeY (j τ)) PhiQ) (τ : UpperHalfPlane) : (Polynomial.aeval (j τ)) (diagPhiQ PhiQ) = ∏ i : Option (ZMod m), (j τ - f m i τ)

G_m(j τ) = ∏_i (j τ − f m i τ): evaluating the diagonal polynomial at j τ recovers the orbit product.

(C2, input) The CM coset relation ∃ i, f m i τ₁₆₃ = j τ₁₆₃

The CM matrix M_n = [[n+1, −41],[1, n]] fixes τ₁₆₃; it decomposes as γ · Acol m n with γ = [[n+1, −1],[1, 0]] ∈ SL(2,ℤ), so j (Acol m n • τ₁₆₃) = j τ₁₆₃.

noncomputable def Chudnovsky.cmGL (n : ℤ) : GL (Fin 2) ℝ

The CM matrix M_n = [[n+1, −41],[1, n]] as an element of GL (Fin 2) ℝ (determinant n² + n + 41 > 0).

Equations

• Chudnovsky.cmGL n = Matrix.GeneralLinearGroup.mkOfDetNeZero !![↑n + 1, -41; 1, ↑n] ⋯

@[simp]

theorem Chudnovsky.val_cmGL (n : ℤ) : ↑(cmGL n) = !![↑n + 1, -41; 1, ↑n]

theorem Chudnovsky.cmGL_det_pos (n : ℤ) : 0 < ↑(Matrix.GeneralLinearGroup.det (cmGL n))

theorem Chudnovsky.cmGL_smul_eq (n : ℤ) : cmGL n • τ₁₆₃ = τ₁₆₃

M_n fixes τ₁₆₃ as a Möbius transformation.

def Chudnovsky.cmGamma (n : ℤ) : Matrix.SpecialLinearGroup (Fin 2) ℤ

The SL(2,ℤ) cofactor γ = [[n+1, −1],[1, 0]] (determinant 1).

Equations

• Chudnovsky.cmGamma n = ⟨!![n + 1, -1; 1, 0], ⋯⟩

theorem Chudnovsky.cmGL_factor {m : ℕ} (n : ℤ) [NeZero m] (hm : ↑m = n ^ 2 + n + 41) : cmGL n = Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) (cmGamma n)) * Acol m n

Coset decomposition M_n = γ · Acol m n (as GL (Fin 2) ℝ), valid when m = n² + n + 41.

theorem Chudnovsky.cm_coset_val {m : ℕ} (n : ℤ) [NeZero m] (hm : ↑m = n ^ 2 + n + 41) : j (Acol m n • τ₁₆₃) = j τ₁₆₃

The b-coset value at τ₁₆₃. j (Acol m n • τ₁₆₃) = j τ₁₆₃.

theorem Chudnovsky.cm_coset_rel {m : ℕ} (n : ℤ) [NeZero m] (hm : ↑m = n ^ 2 + n + 41) : ∃ (i : Option (ZMod m)), f m i τ₁₆₃ = j τ₁₆₃

(C2, input): the CM coset relation. For m = n² + n + 41, some coset value coincides with j τ₁₆₃: f m (some (n : ZMod m)) τ₁₆₃ = j τ₁₆₃.

(C4)/(C5) Form-theory helpers (binary quadratic forms of a CM point)

Added to the Chudnovsky.QF namespace of QuadraticPoints.lean / FormReduction.lean. They provide: a fixing integer matrix of a point yields a definite integer form; two forms with a common root are proportional; a primitive representative exists; and the mod-4 constraint disc ≤ −3.

theorem Chudnovsky.QF.disc_neg_of_isRoot {F : BQF} {τ : UpperHalfPlane} (ha : F.a ≠ 0) (h : IsRoot F τ) : disc F < 0

A binary quadratic form with a ≠ 0 whose root lies in ℍ (a non-real number) has negative discriminant.

theorem Chudnovsky.QF.root_prop {F G : BQF} {τ : UpperHalfPlane} (hF : IsRoot F τ) (hG : IsRoot G τ) : F.a * G.b = G.a * F.b ∧ F.a * G.c = G.a * F.c

Two forms with a common root τ ∈ ℍ are proportional: F.a·G.b = G.a·F.b and F.a·G.c = G.a·F.c.

theorem Chudnovsky.QF.exists_int_mult {F G : BQF} {τ : UpperHalfPlane} (hFp : IsPrimitive F) (hFa : F.a ≠ 0) (hF : IsRoot F τ) (hG : IsRoot G τ) : ∃ (l : ℤ), G.a = l * F.a ∧ G.b = l * F.b ∧ G.c = l * F.c

If F is primitive with a root τ, any form G with the same root is an integer multiple of F.

theorem Chudnovsky.QF.exists_primitive_isRoot {F : BQF} {τ : UpperHalfPlane} (hpd : IsPosDef F) (hroot : IsRoot F τ) : ∃ (F₀ : BQF), IsPrimitive F₀ ∧ IsPosDef F₀ ∧ IsRoot F₀ τ

A positive-definite form has a primitive positive-definite representative with the same root.

theorem Chudnovsky.QF.disc_le_neg_three {F : BQF} (hpd : IsPosDef F) : disc F ≤ -3

A positive-definite form has discriminant ≤ −3 (its discriminant is ≡ 0 or 1 mod 4 and negative).

(C4) From a coset coincidence to a fixing integer matrix and a definite form

theorem Chudnovsky.fixes_of_coset {e f g : ℤ} (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) {Aτ τ' : UpperHalfPlane} (hW : ↑Aτ = (↑e * ↑τ' + ↑f) / ↑g) (hg : ↑g ≠ 0) (hfix : γ • Aτ = τ') : ∃ (p : ℤ) (q : ℤ) (r : ℤ) (s : ℤ), QF.Fixes p q r s τ' ∧ p * s - q * r = e * g

Fixing matrix from a coset factorization. If γ ∈ SL(2,ℤ) sends the coset point Aτ (with Aτ = (e·τ' + f)/g) to τ', then the integer matrix γ · [[e,f],[0,g]] fixes τ'; its entries give a QF.Fixes relation of determinant e·g.

theorem Chudnovsky.exists_fixes_of_coincidence {m : ℕ} [Fact (Nat.Prime m)] {τ' : UpperHalfPlane} {i : Option (ZMod m)} (h : f m i τ' = j τ') : ∃ (p : ℤ) (q : ℤ) (r : ℤ) (s : ℤ), QF.Fixes p q r s τ' ∧ p * s - q * r = ↑m

(C4). A coset coincidence f m i τ′ = j τ′ yields integers p q r s with a QF.Fixes relation of determinant m.

theorem Chudnovsky.exists_form_of_coincidence {m : ℕ} [Fact (Nat.Prime m)] {τ' : UpperHalfPlane} {i : Option (ZMod m)} (h : f m i τ' = j τ') : ∃ (F : QF.BQF) (t : ℤ), QF.IsPosDef F ∧ QF.IsRoot F τ' ∧ QF.disc F = t ^ 2 - 4 * ↑m

(C4), packaged. A coset coincidence at τ′ produces a positive-definite integer form rooted at τ′ of discriminant t² − 4m.

(C5)/(C6) The three-prime bridge: τ′ is Γ-equivalent to τ₁₆₃

theorem Chudnovsky.cm_bridge {τ' : UpperHalfPlane} (h41 : ∃ (i : Option (ZMod 41)), f 41 i τ' = j τ') (h43 : ∃ (i : Option (ZMod 43)), f 43 i τ' = j τ') (h61 : ∃ (i : Option (ZMod 61)), f 61 i τ' = j τ') : ∃ (M : Matrix.SpecialLinearGroup (Fin 2) ℤ), M • τ' = τ₁₆₃

(C5)+(C6). If τ′ carries a coset coincidence for each of m ∈ {41, 43, 61}, then τ′ is SL(2,ℤ)-equivalent to τ₁₆₃.

(C1)–(C3) Vanishing of Φ_m(x, x) at roots, and the coincidence at τ′

theorem Chudnovsky.phi_coincidence (n : ℤ) (mm : ℕ) [NeZero mm] [Fact (Nat.Prime mm)] (hm : ↑mm = n ^ 2 + n + 41) {x : ℂ} (hx : (Polynomial.aeval x) (minpoly ℚ (j τ₁₆₃)) = 0) {τ' : UpperHalfPlane} (hτ' : j τ' = x) : ∃ (i : Option (ZMod mm)), f mm i τ' = j τ'

(C2)+(C3). For a root x of minpoly ℚ j₀ and τ′ with j τ′ = x, each prime m = n² + n + 41 yields a coset coincidence f m i τ′ = j τ′.

(C7) Rationality of j τ₁₆₃

theorem Chudnovsky.j_τ₁₆₃_rational_of (hsurj : Function.Surjective j) (hint : IsIntegral ℤ (j τ₁₆₃)) : ∃ (r : ℚ), j τ₁₆₃ = ↑r

The three-prime argument (§4.2). Assuming surjectivity of j and integrality of j τ₁₆₃, the value j τ₁₆₃ is rational.