Prime-discriminant factorization of a fundamental discriminant #
FundamentalDiscriminant/Basic supplies the synthesis half of the prime-discriminant/
fundamental-discriminant correspondence: a product of distinct prime discriminants with at most
one even value is a fundamental discriminant. This file supplies the analysis half, the
converse existence statement: every fundamental discriminant D is a product of a finite set of
prime discriminants, at most one of which is even.
The factorization is unique once its factors are required to be distinct. Its proof first matches
the odd factors through the unique rational prime below each prime discriminant. After cancelling
their common product, the remaining factors belong to the three-element set {-4, 8, -8}; its
eight subsets have pairwise distinct products, so the even factors match as well.
This is the classical prime-discriminant factorization; see D. A. Cox, Primes of the Form x² + ny², §3.B and §6.A, and F. Lemmermeyer, Reciprocity Laws: From Euler to Eisenstein, §2.2.
This is a prerequisite for the genus-field layer, which attaches a family of prime discriminants
to a quadratic field ℚ(√d): the square-class independence and degree theorems of
Multiquadratic/Prime/Discriminant/Independence.lean apply to such a family, giving a
degree-2ᵗ multiquadratic compositum. For negative radicands,
isGenusField_candidateGenusField identifies that compositum with the genus field; the real case
remains future work. This file only supplies the factorization the family comes from.
The engine is prod_oddPrimeDiscriminant_primeFactors_eq: for an odd squarefree x ≡ 1 (mod 4),
the product of the odd prime discriminants p* over the prime factors p of x is x itself.
The two sides share an absolute value (each p* has |p*| = p, and x is squarefree) and are
both ≡ 1 (mod 4), so they agree by sign uniqueness. The three shapes of a fundamental
discriminant — odd, 4 · odd, 8 · odd — then differ only in the single even prime discriminant
(-4, -8, 8) prepended to that odd product.
Main results #
TauCeti.Multiquadratic.IsFundamentalDiscriminant.exists_finset_primeDiscriminant: every fundamental discriminant is a product of a finite set of prime discriminants with at most one even value — the converse ofisFundamentalDiscriminant_prod.TauCeti.Multiquadratic.finset_primeDiscriminant_eq_of_prod_eq: two finite sets of prime discriminants with the same product have the same factors.TauCeti.Multiquadratic.IsFundamentalDiscriminant.existsUnique_finset_primeDiscriminant: every fundamental discriminant has a unique factorization into a finite set of prime discriminants.
Analysis half of the prime-discriminant correspondence. Every fundamental discriminant
D is a product of a finite set of prime discriminants, at most one of which is even. This is the
converse of TauCeti.Multiquadratic.isFundamentalDiscriminant_prod.
Uniqueness of a prime-discriminant factorization. Two finite sets of prime discriminants are equal when their products are equal.
Odd factors are determined by their unique underlying rational prime. Once those common factors
are cancelled from the product equality, each remaining factor belongs to {-4, 8, -8}; the
products of the eight possible subsets are distinct, so the even factors match too.
Unique prime-discriminant factorization of a fundamental discriminant. Every fundamental discriminant is the product of a unique finite set of prime discriminants.