Prime classification, part 4: the ramified case

Thesis. §3.2, Proposition 3.2.1 — the ramified branch: a rational prime p ramifies in O_d exactly when p ∣ d. Algebraically, (p) fails to be a radical ideal: O/(p) acquires a nonzero nilpotent (the dual-numbers picture).

This file proves:

• tau_sq_mem_span_p_of_p_dvd_d — τ² ∈ (p) when p ∣ d
• tau_not_mem_span_p — τ ∉ (p) (always; τ is a basis element)
• span_p_not_isRadical_of_p_dvd_d — together: (p) is not radical
• prime_ramified_iff — (p) not radical ↔ p ∣ d

The reverse direction of prime_ramified_iff (p ∤ d ⇒ (p) radical) uses the private helper polyMod_squarefree_of_not_p_dvd_d, transported across the ring iso of QuotientIso.lean.

Divergence from thesis. "Ramified" is phrased here as the precise statement ¬ (p).IsRadical, with τ as an explicit order-2 nilpotent witness. The reverse direction reduces to squarefreeness of polyMod d p and transports IsReduced across quadraticOrderModPEquivPolyModQuot, in place of the thesis's hand computation. Mathematically the same as Prop 3.2.1.

theorem QuadraticOrder.tau_sq_mem_span_p_of_p_dvd_d {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) (hpd : ↑p ∣ d) : tau ^ 2 ∈ Ideal.span {↑p}

Ramification witness: when p ∣ d (with p ≠ 2, d ≡ 0 ∨ 1 (mod 4)), τ² lies in (p) ⊆ QuadraticOrder d. Combined with τ ∉ (p) (which holds generally because τ is a Z-basis element), this exhibits τ + (p) as a nonzero nilpotent of order 2 in QuadraticOrder d / (p) — the algebraic fingerprint of ramification of p in QuadraticOrder d.

theorem QuadraticOrder.tau_not_mem_span_p {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] : tau ∉ Ideal.span {↑p}

τ is not in the ideal (p) of QuadraticOrder d for any prime p. This holds because τ is the second ℤ-basis element of QuadraticOrder d (the first being 1), so its τ-coordinate is 1, which is not a multiple of p ≥ 2.

Together with tau_sq_mem_span_p_of_p_dvd_d, this shows that when p ∣ d, the image of τ in QuadraticOrder d / (p) is a nonzero element with τ² = 0 — a genuine order-2 nilpotent witnessing ramification.

theorem QuadraticOrder.span_p_not_isRadical_of_p_dvd_d {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) (hpd : ↑p ∣ d) : ¬(Ideal.span {↑p}).IsRadical

Ramified-direction radical-witness: when p ∣ d (with p ≠ 2, d ≡ 0 ∨ 1 (mod 4)), the ideal (p) in QuadraticOrder d is NOT a radical ideal. The witness is τ: τ² ∈ (p) (by tau_sq_mem_span_p_of_p_dvd_d) but τ ∉ (p) (by tau_not_mem_span_p). This is the algebraic fingerprint of ramification — the quotient QuadraticOrder d / (p) has a nonzero nilpotent.

theorem QuadraticOrder.prime_ramified_iff {d : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hp2 : p ≠ 2) (hd : d % 4 = 0 ∨ d % 4 = 1) : ¬(Ideal.span {↑p}).IsRadical ↔ ↑p ∣ d

Issue #7's ramified iff at the ideal level: the ideal (p) fails to be radical in QuadraticOrder d exactly when p ∣ d. The forward direction (p ∣ d → ¬ IsRadical) is span_p_not_isRadical_of_p_dvd_d. The reverse (p ∤ d → IsRadical) is proved by transporting squarefreeness of polyMod d p (from polyMod_squarefree_of_not_p_dvd_d) along the ring isomorphism quadraticOrderModPEquivPolyModQuot.