Binary quadratic forms and CM points (Phase C, Track 3)

This file develops the elementary theory of integral binary quadratic forms f = (a, b, c) (meaning a X² + b XY + c Y²) together with their action of GL₂(ℤ)/SL₂(ℤ), the discriminant and content, and the correspondence with CM points — points τ ∈ ℍ satisfying a τ² + b τ + c = 0.

It is the arithmetic input to FormReduction.lean (the reduction algorithm and the decide-enumeration of reduced forms of discriminant −163) and to the three-prime rationality argument of PhaseC-PLAN.md §4.2, whose chunk (C5) consumes:

• the discriminant disc f = b² − 4ac and its invariance under SL₂ (disc_act);
• primitivity (IsPrimitive) and its preservation under GL₂(ℤ) (IsPrimitive.act);
• the fixed-point / ℚ[Λ]-algebra classification: an integer matrix fixing a CM point τ of a primitive form is p·I + k·(form matrix), with det = p² + b p k + a c k² (fixes_iff, det_of_fixes).

Conventions match ComplexMult.lean: at τ₁₆₃ the CM relation is 41 − τ + τ² = 0, i.e. the form (a, b, c) = (1, −1, 41), disc = −163.

The GL₂ action is the classical right action on forms, (f · M)(X, Y) = f(pX + qY, rX + sY) for M = ![![p, q], ![r, s]]; it is packaged as BQF.act f p q r s taking the four entries directly (avoiding matrix-coercion churn).

structure Chudnovsky.QF.BQF : Type

An integral binary quadratic form a X² + b XY + c Y², recorded as its coefficient triple (a, b, c).

• a : ℤ

  The X² coefficient.

• b : ℤ

  The XY coefficient.

• c : ℤ

  The Y² coefficient.

theorem Chudnovsky.QF.BQF.ext_iff {x y : BQF} : x = y ↔ x.a = y.a ∧ x.b = y.b ∧ x.c = y.c

theorem Chudnovsky.QF.BQF.ext {x y : BQF} (a : x.a = y.a) (b : x.b = y.b) (c : x.c = y.c) : x = y

def Chudnovsky.QF.instDecidableEqBQF.decEq (x✝ x✝¹ : BQF) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Chudnovsky.QF.instDecidableEqBQF : DecidableEq BQF

Equations

• Chudnovsky.QF.instDecidableEqBQF = Chudnovsky.QF.instDecidableEqBQF.decEq

def Chudnovsky.QF.disc (f : BQF) : ℤ

The discriminant b² − 4ac.

Equations

• Chudnovsky.QF.disc f = f.b ^ 2 - 4 * f.a * f.c

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

A form is positive definite when a > 0 and disc < 0 (then c > 0 too).

Equations

• Chudnovsky.QF.IsPosDef f = (0 < f.a ∧ Chudnovsky.QF.disc f < 0)

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

A form is primitive when its coefficients have no common non-unit divisor.

Equations

• Chudnovsky.QF.IsPrimitive f = ∀ (d : ℤ), d ∣ f.a → d ∣ f.b → d ∣ f.c → IsUnit d

def Chudnovsky.QF.act (f : BQF) (p q r s : ℤ) : BQF

The right GL₂-action on forms: (f · ![![p,q],![r,s]]).

Equations

• Chudnovsky.QF.act f p q r s = { a := f.a * p ^ 2 + f.b * p * r + f.c * r ^ 2, b := 2 * f.a * p * q + f.b * (p * s + q * r) + 2 * f.c * r * s, c := f.a * q ^ 2 + f.b * q * s + f.c * s ^ 2 }

@[simp]

theorem Chudnovsky.QF.act_a (f : BQF) (p q r s : ℤ) : (act f p q r s).a = f.a * p ^ 2 + f.b * p * r + f.c * r ^ 2

@[simp]

theorem Chudnovsky.QF.act_b (f : BQF) (p q r s : ℤ) : (act f p q r s).b = 2 * f.a * p * q + f.b * (p * s + q * r) + 2 * f.c * r * s

@[simp]

theorem Chudnovsky.QF.act_c (f : BQF) (p q r s : ℤ) : (act f p q r s).c = f.a * q ^ 2 + f.b * q * s + f.c * s ^ 2

@[simp]

theorem Chudnovsky.QF.act_one (f : BQF) : act f 1 0 0 1 = f

The identity matrix acts trivially.

theorem Chudnovsky.QF.disc_act (f : BQF) (p q r s : ℤ) : disc (act f p q r s) = (p * s - q * r) ^ 2 * disc f

Discriminant transforms by the square of the determinant. In particular for SL₂ (p s − q r = 1) the discriminant is invariant.

theorem Chudnovsky.QF.act_act (f : BQF) (p q r s p' q' r' s' : ℤ) : act (act f p q r s) p' q' r' s' = act f (p * p' + q * r') (p * q' + q * s') (r * p' + s * r') (r * q' + s * s')

Composition of two acts is the act of the matrix product.

theorem Chudnovsky.QF.act_act_inv (f : BQF) {p q r s : ℤ} (hdet : p * s - q * r = 1) : act (act f p q r s) s (-q) (-r) p = f

Acting by an SL₂-matrix and then by its inverse ![![s,-q],![-r,p]] returns f.

theorem Chudnovsky.QF.dvd_act_of_dvd {d : ℤ} {f : BQF} (ha : d ∣ f.a) (hb : d ∣ f.b) (hc : d ∣ f.c) (p q r s : ℤ) : d ∣ (act f p q r s).a ∧ d ∣ (act f p q r s).b ∧ d ∣ (act f p q r s).c

A common divisor of the coefficients divides the coefficients of any act.

theorem Chudnovsky.QF.IsPrimitive.act {f : BQF} (hf : IsPrimitive f) {p q r s : ℤ} (hdet : p * s - q * r = 1) : IsPrimitive (QF.act f p q r s)

Primitivity is preserved by SL₂ (indeed GL₂(ℤ)).

CM points: roots of a form in the upper half-plane

def Chudnovsky.QF.IsRoot (f : BQF) (τ : UpperHalfPlane) : Prop

τ ∈ ℍ is a root of the form f when a τ² + b τ + c = 0.

Equations

• Chudnovsky.QF.IsRoot f τ = (↑f.a * ↑τ ^ 2 + ↑f.b * ↑τ + ↑f.c = 0)

theorem Chudnovsky.QF.real_lin_eq_zero (τ : UpperHalfPlane) {α β : ℝ} (h : ↑α * ↑τ + ↑β = 0) : α = 0 ∧ β = 0

A real linear relation α·τ + β = 0 at a point of ℍ forces α = 0 (and then β = 0): the imaginary part gives α · Im τ = 0.

theorem Chudnovsky.QF.int_lin_eq_zero (τ : UpperHalfPlane) {α β : ℤ} (h : ↑α * ↑τ + ↑β = 0) : α = 0 ∧ β = 0

An integer linear relation α·τ + β = 0 at a point of ℍ forces α = β = 0.

theorem Chudnovsky.QF.IsPosDef.c_pos {f : BQF} (hf : IsPosDef f) : 0 < f.c

For a positive-definite form, c > 0 as well (4ac = b² − disc > 0).

theorem Chudnovsky.QF.sq_two_a_root {f : BQF} {τ : UpperHalfPlane} (h : IsRoot f τ) : (2 * ↑f.a * ↑τ + ↑f.b) ^ 2 = ↑(disc f)

The square-completion identity (2aτ + b)² = disc f for a root τ of f.

theorem Chudnovsky.QF.root_unique {f : BQF} (hf : IsPosDef f) {τ τ' : UpperHalfPlane} (h : IsRoot f τ) (h' : IsRoot f τ') : τ = τ'

Uniqueness of the CM point of a positive-definite form. Two roots in ℍ of the same positive-definite form are equal (both are the root with positive imaginary part).

The fixed-point (ℚ[Λ]) algebra

An integer matrix ![![p,q],![r,s]] fixes τ ∈ ℍ (as a Möbius transformation) when p τ + q = τ (r τ + s), i.e. r τ² + (s − p) τ − q = 0. For a root τ of a primitive positive-definite form f = (a,b,c), the fixing matrices are exactly p·I + k·M_f where M_f = ![![0,−c],![a,b]] is the companion matrix of f; the determinant is the norm form p² + b p k + a c k². This is the ℚ[Λ]-algebra fact consumed by PhaseC-PLAN.md §4.2 (C5) and §5.1 step 4.

def Chudnovsky.QF.Fixes (p q r s : ℤ) (τ : UpperHalfPlane) : Prop

The fixing relation p τ + q = τ (r τ + s), division-free.

Equations

• Chudnovsky.QF.Fixes p q r s τ = (↑p * ↑τ + ↑q = ↑τ * (↑r * ↑τ + ↑s))

theorem Chudnovsky.QF.bezout_of_primitive {f : BQF} (hf : IsPrimitive f) : ∃ (u : ℤ) (v : ℤ) (w : ℤ), u * f.a + v * f.b + w * f.c = 1

A primitive form admits a Bézout relation among its coefficients.

theorem Chudnovsky.QF.fixes_classification {f : BQF} (hf : IsPrimitive f) (hpd : IsPosDef f) {p q r s : ℤ} {τ : UpperHalfPlane} (hroot : IsRoot f τ) (hfix : Fixes p q r s τ) : ∃ (k : ℤ), r = k * f.a ∧ s - p = k * f.b ∧ q = -(k * f.c)

Fixed-matrix classification. If an integer matrix ![![p,q],![r,s]] fixes a root τ of a primitive positive-definite form f, then there is k : ℤ with r = k·a, s − p = k·b, q = −k·c.

theorem Chudnovsky.QF.det_of_fixes {f : BQF} (hf : IsPrimitive f) (hpd : IsPosDef f) {p q r s : ℤ} {τ : UpperHalfPlane} (hroot : IsRoot f τ) (hfix : Fixes p q r s τ) : ∃ (k : ℤ), p * s - q * r = p ^ 2 + f.b * p * k + f.a * f.c * k ^ 2

Determinant is the norm form. For a fixing matrix as classified above, det = p s − q r = p² + b p k + a c k² — the value of the norm form of the order at (p, k), with disc = b² − 4ac.