Even prime discriminants

The genus-field layer of the multiquadratic roadmap uses the prime discriminants dividing a quadratic discriminant. The odd-prime normalization p* is developed in TauCeti.NumberTheory.Multiquadratic.Prime.Discriminant.Basic; this file records the complementary 2-adic list:

• -4, represented by the squarefree radicand -1;
• 8, represented by the squarefree radicand 2;
• -8, represented by the squarefree radicand -2.

The quotient by 4 is the radicand whose square root generates the same quadratic field as the corresponding even prime discriminant. This is the small arithmetic API needed before the later genus-field package can form the multiquadratic compositum of the ℚ(√p*) factors.

Main definitions and results

• TauCeti.Multiquadratic.IsEvenPrimeDiscriminant: membership in the finite set {-4, 8, -8}.
• TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand: the radicand D / 4.
• TauCeti.Multiquadratic.evenPrimeDiscriminant_eq_four_mul_radicand: reconstructs D from its radicand for the three even prime discriminants.
• TauCeti.Multiquadratic.squarefree_evenPrimeDiscriminantRadicand: the radicand is squarefree.
• TauCeti.Multiquadratic.not_isSquare_evenPrimeDiscriminantRadicand_rat: the associated rational radicand is not a square.

def TauCeti.Multiquadratic.IsEvenPrimeDiscriminant (D : ℤ) : Prop

The three even prime discriminants: -4, 8, and -8.

Equations

• TauCeti.Multiquadratic.IsEvenPrimeDiscriminant D = (D = -4 ∨ D = 8 ∨ D = -8)

theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_iff {D : ℤ} : IsEvenPrimeDiscriminant D ↔ D = -4 ∨ D = 8 ∨ D = -8

The defining disjunction for IsEvenPrimeDiscriminant.

@[simp]

theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_neg_four : IsEvenPrimeDiscriminant (-4)

@[simp]

theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_eight : IsEvenPrimeDiscriminant 8

@[simp]

theorem TauCeti.Multiquadratic.isEvenPrimeDiscriminant_neg_eight : IsEvenPrimeDiscriminant (-8)

def TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand (D : ℤ) : ℤ

The squarefree radicand associated to an even prime discriminant. For D = -4, 8, -8 this gives respectively -1, 2, -2.

Equations

• TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand D = D / 4

@[simp]

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_neg_four : evenPrimeDiscriminantRadicand (-4) = -1

@[simp]

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eight : evenPrimeDiscriminantRadicand 8 = 2

@[simp]

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_neg_eight : evenPrimeDiscriminantRadicand (-8) = -2

theorem TauCeti.Multiquadratic.evenPrimeDiscriminant_eq_four_mul_radicand {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : D = 4 * evenPrimeDiscriminantRadicand D

An even prime discriminant is four times its associated squarefree radicand.

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eq_neg_one_or_eq_two_or_eq_neg_two {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : evenPrimeDiscriminantRadicand D = -1 ∨ evenPrimeDiscriminantRadicand D = 2 ∨ evenPrimeDiscriminantRadicand D = -2

The associated squarefree radicand of an even prime discriminant is one of -1, 2, or -2.

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_natAbs_eq_one_or_two {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : (evenPrimeDiscriminantRadicand D).natAbs = 1 ∨ (evenPrimeDiscriminantRadicand D).natAbs = 2

The absolute value of the radicand attached to an even prime discriminant is 1 or 2.

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_ne_zero {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : evenPrimeDiscriminantRadicand D ≠ 0

The radicand attached to an even prime discriminant is nonzero.

theorem TauCeti.Multiquadratic.squarefree_evenPrimeDiscriminantRadicand {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : Squarefree (evenPrimeDiscriminantRadicand D)

The radicand attached to an even prime discriminant is squarefree.

theorem TauCeti.Multiquadratic.two_dvd_evenPrimeDiscriminant {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : 2 ∣ D

The even prime discriminants themselves are even.

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_mod_four_eq_three_or_two {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : evenPrimeDiscriminantRadicand D % 4 = 3 ∨ evenPrimeDiscriminantRadicand D % 4 = 2

The radicand attached to an even prime discriminant is congruent to -1 or 2 modulo 4.

theorem TauCeti.Multiquadratic.not_isSquare_evenPrimeDiscriminantRadicand_rat {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : ¬IsSquare ↑(evenPrimeDiscriminantRadicand D)

The rational radicand associated to an even prime discriminant is not a square.

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eq_neg_one_iff {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : evenPrimeDiscriminantRadicand D = -1 ↔ D = -4

The discriminant -4 gives the radicand -1.

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eq_two_iff {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : evenPrimeDiscriminantRadicand D = 2 ↔ D = 8

The discriminant 8 gives the radicand 2.

theorem TauCeti.Multiquadratic.evenPrimeDiscriminantRadicand_eq_neg_two_iff {D : ℤ} (hD : IsEvenPrimeDiscriminant D) : evenPrimeDiscriminantRadicand D = -2 ↔ D = -8

The discriminant -8 gives the radicand -2.