Prime classification, part 5: the split case

Thesis. §3.2, Proposition 3.2.1 — the split branch: a rational prime p splits in O_d (factors as a product of two distinct primes) exactly when the Legendre symbol (d/p) = 1. Ideal-theoretically: (p) is radical but not maximal.

This file proves:

• prime_split_iff — (p) radical ∧ ¬ maximal ↔ (d/p) = 1

This is the third branch of the prime-classification trichotomy, completing prime_inert_iff (Inert.lean) and prime_ramified_iff (Ramified.lean).

Divergence from thesis. No new ideal-theory work: the proof is pure logical composition of the inert and ramified iffs with the trichotomy legendreSym p d ∈ {-1, 0, 1}. The "split = radical-but-not-maximal" framing of the quotient O/(p) ≅ 𝔽ₚ × 𝔽ₚ is the Lean-idiomatic restatement of the thesis's "p factors as two distinct primes".

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

Issue #7's split iff at the ideal level: the ideal (p) is radical but not maximal in QuadraticOrder d — equivalently, (p) factors as a product of two distinct primes (the "split" case) — iff the Legendre symbol (d/p) = 1. This is the remaining case of the prime-classification iff trichotomy, complementing prime_inert_iff ((d/p) = -1) and prime_ramified_iff ((d/p) = 0). The proof composes the latter two with the trichotomy of legendreSym p d ∈ {-1, 0, 1}.