Layer 2a: Prime classification in QuadraticOrder d #
Thesis. ยง3.2, Proposition 3.2.1 and Remark 3.2.3 โ the split / inert /
ramified trichotomy of a rational prime p in the order O_d, governed by the
Kronecker / Legendre symbol (d/p).
This module is the aggregator for the prime-classification development, which
is split one-result-per-concern across Prime/:
| file | content | thesis |
|---|---|---|
Prime/PolyMod | polyMod d p, root โ Legendre bridge | Prop 3.2.1 (poly) |
Prime/QuotientIso | O/(p) โ
๐ฝโ[X]/(polyMod), โ
๐ฝโ[X]/(Xยฒ) | proof device |
Prime/Inert | (p) maximal โ (d/p) = -1 | Prop 3.2.1 inert |
Prime/Ramified | (p) not radical โ p โฃ d | Prop 3.2.1 ramified |
Prime/Split | (p) radical, not maximal โ (d/p) = 1 | Prop 3.2.1 split |
See Prime/QuotientIso.lean for the main divergence from the thesis: the
whole trichotomy is routed through one ring isomorphism rather than the
thesis's explicit index computations.