Reduction of binary quadratic forms of discriminant −163 (Phase C, Track 3)

This file provides the decide-heavy combinatorial inputs of PhaseC-PLAN.md §4.2:

• SL₂-equivalence of forms (Equiv), an equivalence relation, with the two generators T (shift b ↦ b + 2an) and S (swap (a,b,c) ↦ (c,−b,a)).
• (C6) enumeration of reduced forms (reduced_disc_neg163): the only positive-definite reduced form of discriminant −163 is (1, ±1, 41) — proved by nlinarith bounding a ≤ 7 followed by interval_cases/omega. Together with the descent exists_reduced_equiv this gives h(−163) = 1 at the level of forms.
• (C5) the three-prime discriminant enumeration (three_prime_N and its ℤ wrapper disc_of_three_relations): the only negative discriminant D₀ for which t² − 4m = D₀ λ² is solvable simultaneously for m ∈ {41, 43, 61} is D₀ = −163. This is the arithmetic heart of the rationality argument; the trap noted in §6.6 ({41,43,47} fails, −43 survives) is what makes the choice of primes load-bearing.

The bridge from these form-level facts to the statement "every CM point of discriminant −163 is Γ-equivalent to τ₁₆₃" additionally needs the SL₂-action on ℍ matched with BQF.act; that analytic bookkeeping is deferred (see the closing TODO).

SL₂-equivalence of forms

def Chudnovsky.QF.Equiv (f g : BQF) : Prop

Two forms are SL₂(ℤ)-equivalent when one is carried to the other by a determinant-1 act.

Equations

• Chudnovsky.QF.Equiv f g = ∃ (p : ℤ) (q : ℤ) (r : ℤ) (s : ℤ), p * s - q * r = 1 ∧ Chudnovsky.QF.act f p q r s = g

theorem Chudnovsky.QF.Equiv.refl (f : BQF) : Equiv f f

theorem Chudnovsky.QF.Equiv.symm {f g : BQF} (h : Equiv f g) : Equiv g f

theorem Chudnovsky.QF.Equiv.trans {f g h : BQF} (hfg : Equiv f g) (hgh : Equiv g h) : Equiv f h

theorem Chudnovsky.QF.Equiv.T (f : BQF) (n : ℤ) : Equiv f (act f 1 n 0 1)

The T-generator: shift (a, b, c) ↦ (a, b + 2an, a n² + b n + c); preserves the form class and (obviously) the discriminant.

theorem Chudnovsky.QF.act_T_a (f : BQF) (n : ℤ) : (act f 1 n 0 1).a = f.a

theorem Chudnovsky.QF.act_T_b (f : BQF) (n : ℤ) : (act f 1 n 0 1).b = f.b + 2 * f.a * n

theorem Chudnovsky.QF.act_T_c (f : BQF) (n : ℤ) : (act f 1 n 0 1).c = f.a * n ^ 2 + f.b * n + f.c

theorem Chudnovsky.QF.Equiv.S (f : BQF) : Equiv f (act f 0 (-1) 1 0)

The S-generator: swap (a, b, c) ↦ (c, −b, a).

theorem Chudnovsky.QF.act_S_a (f : BQF) : (act f 0 (-1) 1 0).a = f.c

theorem Chudnovsky.QF.act_S_b (f : BQF) : (act f 0 (-1) 1 0).b = -f.b

theorem Chudnovsky.QF.act_S_c (f : BQF) : (act f 0 (-1) 1 0).c = f.a

theorem Chudnovsky.QF.Equiv.disc_eq {f g : BQF} (h : Equiv f g) : disc f = disc g

Equivalent forms have equal discriminant.

theorem Chudnovsky.QF.Equiv.isPrimitive {f g : BQF} (h : Equiv f g) (hf : IsPrimitive f) : IsPrimitive g

Equivalence preserves primitivity.

Reduced forms of discriminant −163

def Chudnovsky.QF.IsReduced (f : BQF) : Prop

A form is reduced when −a ≤ b ≤ a ≤ c (the loose convention; both (1,1,41) and (1,−1,41) count, and they are T-equivalent).

Equations

• Chudnovsky.QF.IsReduced f = (-f.a ≤ f.b ∧ f.b ≤ f.a ∧ f.a ≤ f.c)

theorem Chudnovsky.QF.reduced_disc_neg163 {f : BQF} (ha : 0 < f.a) (hred : IsReduced f) (hdisc : disc f = -163) : f = { a := 1, b := -1, c := 41 } ∨ f = { a := 1, b := 1, c := 41 }

(C6) Enumeration. The only positive-definite reduced forms of discriminant −163 are (1, −1, 41) and (1, 1, 41).

The reduction descent: every positive-definite form is equivalent to a reduced one

theorem Chudnovsky.QF.exists_reduced_equiv (f : BQF) (hf : IsPosDef f) : ∃ (g : BQF), Equiv f g ∧ IsPosDef g ∧ IsReduced g

Existence of a reduced representative. Every positive-definite form is SL₂(ℤ)-equivalent to a reduced positive-definite form.

theorem Chudnovsky.QF.equiv_of_disc_neg163 {f : BQF} (hpd : IsPosDef f) (hdisc : disc f = -163) : Equiv f { a := 1, b := -1, c := 41 } ∨ Equiv f { a := 1, b := 1, c := 41 }

(C6), form level. Every positive-definite form of discriminant −163 is SL₂(ℤ)-equivalent to (1, −1, 41) or (1, 1, 41) — the two (T-related) presentations of the class of τ₁₆₃. This is h(−163) = 1 for forms.

(C5) The three-prime discriminant enumeration

For an integer matrix of determinant m fixing a CM point of primitive discriminant D₀, the trace t and the multiplier λ satisfy t² − 4m = D₀ λ² (= disc · λ², see QuadraticPoints.det_of_fixes). The following finite computation shows that D₀ = −163 is the only negative discriminant solvable for all of m ∈ {41, 43, 61}.

def Chudnovsky.QF.reprN (m d : ℕ) : Bool

Whether D₀ = −(d) is representable as t² − 4m = D₀ λ² within the (generous) search box |t| ≤ 15, 1 ≤ λ ≤ 9 that contains every genuine solution (|t|² < 4m ≤ 244 and |D₀| ≥ 3 ⇒ λ² ≤ 4m/3 < 82). Phrased over ℕ for a fast kernel decide.

Equations

• Chudnovsky.QF.reprN m d = decide (∃ t ∈ Finset.range 16, ∃ l ∈ Finset.Icc 1 9, 4 * m - t ^ 2 = d * l ^ 2 ∧ t ^ 2 ≤ 4 * m)

theorem Chudnovsky.QF.three_prime_N (d : ℕ) : d ∈ Finset.Icc 1 244 → reprN 41 d = true → reprN 43 d = true → reprN 61 d = true → d = 163

(C5), computational core. The only d ∈ [1, 244] simultaneously representable at m = 41, 43, 61 is d = 163 (i.e. D₀ = −163). The {41,43,47} trap of §6.6 is exactly that d = 43 would also survive there; here it does not. Proved in four range chunks so each decide stays within the default recursion depth.

theorem Chudnovsky.QF.disc_of_three_relations {D0 : ℤ} (hD3 : D0 ≤ -3) {t1 l1 t2 l2 t3 l3 : ℤ} (hl1 : l1 ≠ 0) (hl2 : l2 ≠ 0) (hl3 : l3 ≠ 0) (h1 : t1 ^ 2 - 4 * 41 = D0 * l1 ^ 2) (h2 : t2 ^ 2 - 4 * 43 = D0 * l2 ^ 2) (h3 : t3 ^ 2 - 4 * 61 = D0 * l3 ^ 2) : D0 = -163

(C5), integer form. The wrapper consumed by the rationality argument: if a common CM point of primitive discriminant D₀ ≤ −3 carries integral matrices of determinants 41, 43, 61 (trace tᵢ, non-zero multiplier λᵢ, so tᵢ² − 4mᵢ = D₀ λᵢ²), then D₀ = −163.

The bridge to ℍ: CM points of discriminant −163 are Γ-equivalent to τ₁₆₃

The SL₂(ℤ)-action on forms BQF.act is matched to the Möbius action on ℍ: if act f p q r s = g (determinant 1) and τ is a root of f, then the point N • τ with N = ![![s,−q],![−r,p]] ∈ SL₂(ℤ) (the inverse matrix) is a root of g. Combined with the form-level classification equiv_of_disc_neg163 and the CM-point uniqueness root_unique, this yields the analytic statement PhaseC-PLAN.md (C6) needs.

theorem Chudnovsky.QF.isRoot_smul {f g : BQF} {p q r s : ℤ} (hdet : p * s - q * r = 1) (hg : act f p q r s = g) {τ : UpperHalfPlane} (hroot : IsRoot f τ) : ∃ (N : Matrix.SpecialLinearGroup (Fin 2) ℤ), IsRoot g (N • τ)

Root transport. If act f p q r s = g with p s − q r = 1 and τ is a root of f, then N • τ is a root of g for the inverse matrix N = ![![s,−q],![−r,p]].

theorem Chudnovsky.QF.isRoot_τ₁₆₃ : IsRoot { a := 1, b := -1, c := 41 } τ₁₆₃

τ₁₆₃ is the root of the reduced form (1, −1, 41) (41 − τ + τ² = 0).

theorem Chudnovsky.QF.cm_disc_neg163_smul_eq_τ₁₆₃ {f : BQF} (hpd : IsPosDef f) (hdisc : disc f = -163) {τ : UpperHalfPlane} (hroot : IsRoot f τ) : ∃ (M : Matrix.SpecialLinearGroup (Fin 2) ℤ), M • τ = τ₁₆₃

(C6), analytic form. Every CM point of a positive-definite form of discriminant −163 is SL₂(ℤ)-equivalent to τ₁₆₃.