Prime classification, part 3: the inert case

Thesis. §3.2, Proposition 3.2.1 — the inert branch: a rational prime p remains prime in O_d exactly when the Legendre symbol (d/p) = -1.

This file proves:

• span_p_isMaximal_iff_irreducible_polyMod — (p) maximal ↔ polyMod d p irreducible (the ideal ↔ polynomial transport)
• prime_inert_iff — (p) maximal ↔ (d/p) = -1

Divergence from thesis. Maximality of (p) is obtained by transporting IsField across quadraticOrderModPEquivPolyModQuot (see QuotientIso.lean) rather than via the thesis's direct index computation in ℤ/pᵏ[x]/g(x).

theorem QuadraticOrder.span_p_isMaximal_iff_irreducible_polyMod (d : ℤ) (p : ℕ) [Fact (Nat.Prime p)] : (Ideal.span {↑p}).IsMaximal ↔ Irreducible (polyMod d p)

The ideal (p) in QuadraticOrder d is maximal iff polyMod d p is irreducible in (ZMod p)[X]. This is the ideal-theoretic inert characterisation: (p) is maximal — equivalently, (p) does not factor in QuadraticOrder d — exactly when its mod-p polynomial form is irreducible over ZMod p.

Combined with polyMod_splits_iff_legendreSym_ne_neg_one (and the field structure on (ZMod p)[X] / (irreducible)), this connects the Legendre symbol (d/p) = -1 characterisation to the ring-theoretic notion that (p) remains prime in QuadraticOrder d.

theorem QuadraticOrder.prime_inert_iff {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) : (Ideal.span {↑p}).IsMaximal ↔ legendreSym p d = -1

Issue #7's inert iff at the ideal level: the ideal (p) is maximal in QuadraticOrder d (i.e. p is "inert") iff the Legendre symbol (d/p) = -1. Direct composition of span_p_isMaximal_iff_irreducible_polyMod with polyMod_irreducible_iff_legendreSym_eq_neg_one.