Legendre symbols of even prime discriminants

The even prime discriminants are -4, 8, and -8, with radicands -1, 2, and -2; they are defined in TauCeti.NumberTheory.Multiquadratic.Prime.Discriminant.Even. Their Legendre symbols at an odd prime q are governed not by quadratic reciprocity but by its supplementary laws: they are the quadratic characters χ₄, χ₈, and χ₈' evaluated at q.

Concretely, for an odd prime q,

• (-1 / q) = χ₄ q, the radicand of -4;
• (2 / q) = χ₈ q, the radicand of 8;
• (-2 / q) = χ₈' q, the radicand of -8.

Since an even prime discriminant D is four times its radicand and 4 is a square, the Legendre symbol of D itself agrees with that of its radicand at every odd prime. Each symbol is therefore decided by a congruence on q modulo 4 or 8: the classical criteria for q to split in ℚ(i), ℚ(√2), and ℚ(√-2).

The odd prime discriminants p*, whose symbols are governed by quadratic reciprocity, are treated in TauCeti.NumberTheory.Multiquadratic.Legendre.PrimeDiscriminant.Basic, and the two cases are combined in TauCeti.NumberTheory.Multiquadratic.Legendre.PrimeDiscriminants.

Main results

• TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminantRadicand expands the Legendre symbol of an even prime-discriminant radicand at an odd prime as the appropriate supplementary character.
• TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminant_eq_legendreSym_radicand shows that an even prime discriminant and its radicand have the same Legendre symbol at every odd prime.
• legendreSym_evenPrimeDiscriminantRadicand_neg_four_eq_one_iff, ..._eight_eq_one_iff, and ..._neg_eight_eq_one_iff give the quadratic-residue (splitting) conditions as congruences on q modulo 4 or 8.
• legendreSym_evenPrimeDiscriminant_neg_four_eq_one_iff, ..._eight_eq_one_iff, and ..._neg_eight_eq_one_iff give the same conditions for the prime discriminants themselves.

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminantRadicand {q : ℕ} [Fact (Nat.Prime q)] {D : ℤ} (hD : IsEvenPrimeDiscriminant D) (hq : q ≠ 2) : legendreSym q (evenPrimeDiscriminantRadicand D) = if D = -4 then ZMod.χ₄ ↑q else if D = 8 then ZMod.χ₈ ↑q else ZMod.χ₈' ↑q

The Legendre symbol of an even prime-discriminant radicand at an odd prime q is the supplementary character attached to that discriminant: χ₄ q for -4 (radicand -1), χ₈ q for 8 (radicand 2), and χ₈' q for -8 (radicand -2).

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminant_eq_legendreSym_radicand {q : ℕ} [Fact (Nat.Prime q)] {D : ℤ} (hD : IsEvenPrimeDiscriminant D) (hq : q ≠ 2) : legendreSym q D = legendreSym q (evenPrimeDiscriminantRadicand D)

An even prime discriminant D and its radicand D / 4 have the same Legendre symbol at every odd prime q: they differ by the square factor 4, which contributes a trivial symbol. This is the form used by the genus-field splitting law, where the prime discriminant D itself is the splitting character.

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminantRadicand_neg_four_eq_one_iff {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) : legendreSym q (evenPrimeDiscriminantRadicand (-4)) = 1 ↔ q % 4 = 1

The radicand -1 of the prime discriminant -4 is a quadratic residue modulo an odd prime q exactly when q ≡ 1 (mod 4); equivalently q splits in ℚ(√-1) = ℚ(i).

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminantRadicand_eight_eq_one_iff {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) : legendreSym q (evenPrimeDiscriminantRadicand 8) = 1 ↔ q % 8 = 1 ∨ q % 8 = 7

The radicand 2 of the prime discriminant 8 is a quadratic residue modulo an odd prime q exactly when q ≡ 1 or 7 (mod 8); equivalently q splits in ℚ(√2).

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminantRadicand_neg_eight_eq_one_iff {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) : legendreSym q (evenPrimeDiscriminantRadicand (-8)) = 1 ↔ q % 8 = 1 ∨ q % 8 = 3

The radicand -2 of the prime discriminant -8 is a quadratic residue modulo an odd prime q exactly when q ≡ 1 or 3 (mod 8); equivalently q splits in ℚ(√-2).

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminantRadicand_eq_one_iff {q : ℕ} [Fact (Nat.Prime q)] {D : ℤ} (hD : IsEvenPrimeDiscriminant D) (hq : q ≠ 2) : legendreSym q (evenPrimeDiscriminantRadicand D) = 1 ↔ if D = -4 then q % 4 = 1 else if D = 8 then q % 8 = 1 ∨ q % 8 = 7 else q % 8 = 1 ∨ q % 8 = 3

The radicand of a variable even prime discriminant is a quadratic residue modulo an odd prime q exactly under the corresponding supplementary congruence condition.

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminant_eq_one_iff {q : ℕ} [Fact (Nat.Prime q)] {D : ℤ} (hD : IsEvenPrimeDiscriminant D) (hq : q ≠ 2) : legendreSym q D = 1 ↔ if D = -4 then q % 4 = 1 else if D = 8 then q % 8 = 1 ∨ q % 8 = 7 else q % 8 = 1 ∨ q % 8 = 3

A variable even prime discriminant is a quadratic residue modulo an odd prime q exactly under the corresponding supplementary congruence condition.

@[simp]

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminant_neg_four_eq_one_iff {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) : legendreSym q (-4) = 1 ↔ q % 4 = 1

The prime discriminant -4 is a quadratic residue modulo an odd prime q exactly when q ≡ 1 (mod 4).

@[simp]

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminant_eight_eq_one_iff {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) : legendreSym q 8 = 1 ↔ q % 8 = 1 ∨ q % 8 = 7

The prime discriminant 8 is a quadratic residue modulo an odd prime q exactly when q ≡ 1 or 7 (mod 8).

@[simp]

theorem TauCeti.Multiquadratic.legendreSym_evenPrimeDiscriminant_neg_eight_eq_one_iff {q : ℕ} [Fact (Nat.Prime q)] (hq : q ≠ 2) : legendreSym q (-8) = 1 ↔ q % 8 = 1 ∨ q % 8 = 3

The prime discriminant -8 is a quadratic residue modulo an odd prime q exactly when q ≡ 1 or 3 (mod 8).