Legendre symbols of odd prime discriminants

The genus-field layer of the multiquadratic roadmap uses the odd prime discriminant p* = (-1)^((p-1)/2) p rather than the bare prime radicand p. This file records the small Legendre-symbol API that makes that normalization usable in the prime-splitting law.

For odd primes p and q, the classical identity (p* / q) = (q / p) is exactly legendreSym q (oddPrimeDiscriminant p) = legendreSym p q. This file packages that result in the shape downstream multiquadratic splitting statements need.

Main results

• TauCeti.Multiquadratic.legendreSym_oddPrimeDiscriminant expands the Legendre symbol of p* at an arbitrary prime q.
• TauCeti.Multiquadratic.legendreSym_oddPrimeDiscriminant_eq_legendreSym proves (p* / q) = (q / p) for odd primes.
• TauCeti.Multiquadratic.legendreSym_oddPrimeDiscriminant_eq_one_iff rewrites the quadratic-residue condition for an odd prime discriminant into the reciprocal symbol.
• TauCeti.Multiquadratic.forall_legendreSym_oddPrimeDiscriminant_eq_one_iff is the indexed-family form used by the multiquadratic splitting law.

theorem TauCeti.Multiquadratic.legendreSym_oddPrimeDiscriminant (p q : ℕ) [Fact (Nat.Prime q)] : legendreSym q (oddPrimeDiscriminant p) = if p % 4 = 1 then legendreSym q ↑p else legendreSym q (-1) * legendreSym q ↑p

Expanding the Legendre symbol of the odd prime discriminant p*. This version does not assume q is odd: in the negative case it leaves the factor legendreSym q (-1) explicit.

theorem TauCeti.Multiquadratic.legendreSym_oddPrimeDiscriminant_of_ne_two (p q : ℕ) [Fact (Nat.Prime q)] (hq : q ≠ 2) : legendreSym q (oddPrimeDiscriminant p) = if p % 4 = 1 then legendreSym q ↑p else ZMod.χ₄ ↑q * legendreSym q ↑p

Expanding the Legendre symbol of p* at an odd prime q, using the supplementary law legendreSym q (-1) = χ₄ q.

@[simp]

theorem TauCeti.Multiquadratic.legendreSym_oddPrimeDiscriminant_eq_legendreSym {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) : legendreSym q (oddPrimeDiscriminant p) = legendreSym p ↑q

For odd primes p and q, the Legendre symbol of the odd prime discriminant p* at q is the reciprocal symbol (q / p). This is the prime-discriminant form of quadratic reciprocity used by genus-field splitting criteria.

theorem TauCeti.Multiquadratic.legendreSym_oddPrimeDiscriminant_eq_one_iff {p q : ℕ} [Fact (Nat.Prime p)] [Fact (Nat.Prime q)] (hp : p ≠ 2) (hq : q ≠ 2) : legendreSym q (oddPrimeDiscriminant p) = 1 ↔ legendreSym p ↑q = 1

The quadratic-residue condition for the odd prime discriminant p* can be read as the reciprocal Legendre symbol (q / p) = 1. This is the form consumed by the multiquadratic prime-splitting law after the genus-field radicands have been normalized to prime discriminants.

theorem TauCeti.Multiquadratic.forall_legendreSym_oddPrimeDiscriminant_eq_one_iff {ι : Type u_1} (p : ι → ℕ) {q : ℕ} [Fact (Nat.Prime q)] (hpprime : ∀ (i : ι), Nat.Prime (p i)) (hpodd : ∀ (i : ι), p i ≠ 2) (hq : q ≠ 2) : (∀ (i : ι), legendreSym q (oddPrimeDiscriminant (p i)) = 1) ↔ ∀ (i : ι), legendreSym (p i) ↑q = 1

Family form of legendreSym_oddPrimeDiscriminant_eq_one_iff: for a family of odd primes p i, the conditions that all odd prime discriminants p i* are quadratic residues modulo an odd prime q are exactly the reciprocal conditions (q / p i) = 1.