Prime classification, part 1: the reduced polynomial polyMod d p

Thesis. §3.2, Proposition 3.2.1 and Remark 3.2.3 — the splitting behaviour of a rational prime p in O_d is governed by the factorisation of the defining polynomial mod p, i.e. by the Kronecker/Legendre symbol (d/p).

This file is the polynomial-level scaffolding for that classification: reduction of poly d mod p, its degree/coefficients, the discriminant identity disc = d (mod p), and the bridge from roots of polyMod to the Legendre symbol:

• polyMod, polyMod_eq, polyMod_monic, polyMod_natDegree, polyMod_coeff_*
• polyMod_discrim_eq — disc(polyMod) = d in ZMod p (needs d ≡ 0,1 mod 4)
• polyMod_exists_root_iff_isSquare_d / …_legendreSym_ne_neg_one
• polyMod_no_root_iff_legendreSym_eq_neg_one (inert criterion)
• legendreSym_eq_zero_iff_dvd (ramified criterion)
• polyMod_splits_iff_legendreSym_ne_neg_one
• polyMod_eq_X_sq_of_p_dvd_d (ramified: polyMod = X²)
• polyMod_exists_two_distinct_roots_of_legendreSym_eq_one (split)
• polyMod_irreducible_iff_legendreSym_eq_neg_one (inert)

The ideal-level consequences are split across QuotientIso.lean (the ring iso), Inert.lean, Split.lean, and Ramified.lean.

Note. This file also carries the shared Mathlib import block for the whole Prime/ directory; the other Prime/* files import this one and inherit it.

noncomputable def QuadraticOrder.polyMod (d : ℤ) (p : ℕ) : Polynomial (ZMod p)

Reduction of the defining polynomial poly d modulo p, as a polynomial in (ZMod p)[X].

Equations

• QuadraticOrder.polyMod d p = Polynomial.map (Int.castRingHom (ZMod p)) (poly d)

theorem QuadraticOrder.polyMod_eq (d : ℤ) (p : ℕ) : polyMod d p = Polynomial.X ^ 2 - Polynomial.C ↑d * Polynomial.X + Polynomial.C ↑((d ^ 2 - d) / 4)

Explicit form: polyMod d p = X² - d·X + ((d² - d)/4) over ZMod p.

theorem QuadraticOrder.polyMod_monic (d : ℤ) (p : ℕ) : (polyMod d p).Monic

The mod-p reduction is monic.

theorem QuadraticOrder.polyMod_natDegree {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] : (polyMod d p).natDegree = 2

The mod-p reduction has degree 2 (requires p prime so ZMod p is nontrivial).

@[simp]

theorem QuadraticOrder.polyMod_coeff_two {d : ℤ} {p : ℕ} : (polyMod d p).coeff 2 = 1

Coefficient of X² in polyMod d p is 1.

@[simp]

theorem QuadraticOrder.polyMod_coeff_one {d : ℤ} {p : ℕ} : (polyMod d p).coeff 1 = -↑d

Coefficient of X in polyMod d p is -d (mod p).

@[simp]

theorem QuadraticOrder.polyMod_coeff_zero {d : ℤ} {p : ℕ} : (polyMod d p).coeff 0 = ↑((d ^ 2 - d) / 4)

Constant coefficient of polyMod d p is (d² - d)/4 (mod p).

theorem QuadraticOrder.polyMod_discrim_eq {d : ℤ} {p : ℕ} (hd : d % 4 = 0 ∨ d % 4 = 1) : discrim 1 (-↑d) ↑((d ^ 2 - d) / 4) = ↑d

Discriminant identity: when d ≡ 0 ∨ 1 (mod 4), the (coefficient-level) discriminant of the monic-quadratic form of polyMod d p equals d in ZMod p. This is the key bridge connecting poly d's splitting behaviour to the Kronecker symbol (d / p).

theorem QuadraticOrder.polyMod_eval {d : ℤ} {p : ℕ} (x : ZMod p) : Polynomial.eval x (polyMod d p) = x ^ 2 - ↑d * x + ↑((d ^ 2 - d) / 4)

Evaluation of polyMod d p at x ∈ ZMod p: a closed-form expansion.

This reduces evaluation to a quadratic expression in x over ZMod p.

theorem QuadraticOrder.polyMod_exists_root_iff_isSquare_d {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) : (∃ (x : ZMod p), Polynomial.eval x (polyMod d p) = 0) ↔ IsSquare ↑d

For p an odd prime and d ≡ 0 ∨ 1 (mod 4), polyMod d p has a root in ZMod p iff d is a quadratic residue mod p (i.e. IsSquare (d : ZMod p)).

This is the polynomial-level bridge connecting poly d's splitting behaviour to the Kronecker / Legendre symbol (d / p).

theorem QuadraticOrder.polyMod_exists_root_iff_legendreSym_ne_neg_one {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) : (∃ (x : ZMod p), Polynomial.eval x (polyMod d p) = 0) ↔ legendreSym p d ≠ -1

polyMod d p has a root in ZMod p iff the Legendre symbol (d/p) is not -1. Equivalently, d is either zero (ramified case) or a quadratic residue (split case) mod p.

theorem QuadraticOrder.polyMod_no_root_iff_legendreSym_eq_neg_one {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) : (¬∃ (x : ZMod p), Polynomial.eval x (polyMod d p) = 0) ↔ legendreSym p d = -1

polyMod d p has no root in ZMod p iff (d/p) = -1 — the inert case.

theorem QuadraticOrder.legendreSym_eq_zero_iff_dvd {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] : legendreSym p d = 0 ↔ ↑p ∣ d

The ramified case: (d/p) = 0 ↔ p ∣ d.

theorem QuadraticOrder.polyMod_splits_iff_exists_root {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] : (polyMod d p).Splits ↔ ∃ (x : ZMod p), Polynomial.eval x (polyMod d p) = 0

A monic-quadratic polynomial in (ZMod p)[X] splits iff it has a root. For polyMod d p this is the bridge from polyMod_exists_root_iff_isSquare_d to the Polynomial.Splits predicate.

theorem QuadraticOrder.polyMod_splits_iff_legendreSym_ne_neg_one {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) : (polyMod d p).Splits ↔ legendreSym p d ≠ -1

polyMod d p splits in (ZMod p)[X] iff the Legendre symbol (d/p) is not -1. This combines polyMod_splits_iff_exists_root with the previously proved polyMod_exists_root_iff_legendreSym_ne_neg_one.

theorem QuadraticOrder.polyMod_eq_X_sq_of_p_dvd_d {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) (hpd : ↑p ∣ d) : polyMod d p = Polynomial.X ^ 2

The ramified case at the polynomial level: when p is an odd prime dividing d (with d ≡ 0 ∨ 1 (mod 4)), the reduction polyMod d p is identically X² in (ZMod p)[X]. In particular it has the unique root 0 with multiplicity 2, witnessing the ramified behaviour of (p) in QuadraticOrder d.

theorem QuadraticOrder.polyMod_exists_two_distinct_roots_of_legendreSym_eq_one {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) (h_split : legendreSym p d = 1) : ∃ (r : ZMod p) (s : ZMod p), r ≠ s ∧ Polynomial.eval r (polyMod d p) = 0 ∧ Polynomial.eval s (polyMod d p) = 0

The split case at the polynomial level: when p is an odd prime, d ≡ 0 ∨ 1 (mod 4), and the Legendre symbol (d/p) = 1 (so d is a non-zero quadratic residue mod p), polyMod d p has two distinct roots in ZMod p. These two roots witness the splitting (p) = P₁ · P₂ in QuadraticOrder d.

theorem QuadraticOrder.polyMod_irreducible_iff_legendreSym_eq_neg_one {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) : Irreducible (polyMod d p) ↔ legendreSym p d = -1

polyMod d p is irreducible in (ZMod p)[X] iff the Legendre symbol (d/p) = -1. Combines the monic-degree-two irreducibility characterisation with the polynomial-level Legendre bridge already established.