Odd prime discriminants

The genus-field layer of the multiquadratic roadmap uses prime discriminants rather than bare squarefree radicands. For an odd prime p, the associated prime discriminant is

• p when p ≡ 1 (mod 4);
• -p when p ≡ 3 (mod 4).

This file records that elementary normalization as a small arithmetic API. The even prime discriminants -4, 8, and -8 are deliberately left to the later quadratic-discriminant packaging; the odd-prime case is the reusable piece needed to turn the roadmap's odd ramified primes into radicands p* satisfying p* ≡ 1 (mod 4).

Main definitions and results

• TauCeti.Multiquadratic.oddPrimeDiscriminant: the integer p if p % 4 = 1, and -p otherwise.
• TauCeti.Multiquadratic.oddPrimeDiscriminant_natAbs: its absolute value is p.
• TauCeti.Multiquadratic.prime_oddPrimeDiscriminant: it is a prime integer.
• TauCeti.Multiquadratic.dvd_oddPrimeDiscriminant_iff: divisibility by p* is the same as divisibility by p.
• TauCeti.Multiquadratic.oddPrimeDiscriminant_mod_four_eq_one: for odd p, it is 1 mod 4.
• TauCeti.Multiquadratic.oddPrimeDiscriminant_eq_neg_one_pow_pred_div_two_mul: the standard formula p* = (-1)^((p-1)/2) p.
• TauCeti.Multiquadratic.oddPrimeDiscriminant_eq_neg_one_pow_div_two_mul: the equivalent formula p* = (-1)^(p/2) p.

def TauCeti.Multiquadratic.oddPrimeDiscriminant (p : ℕ) : ℤ

The odd prime discriminant p*: p when p % 4 = 1 and -p otherwise (so the value is -p for every p with p % 4 ≠ 1, including even inputs). The p ≡ 3 (mod 4) reading of the second case is the intended one for odd primes. The primality hypothesis is not part of the definition so that the expression rewrites by computation; the API below supplies the prime-specific facts.

Equations

• TauCeti.Multiquadratic.oddPrimeDiscriminant p = if p % 4 = 1 then ↑p else -↑p

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_def (p : ℕ) : oddPrimeDiscriminant p = if p % 4 = 1 then ↑p else -↑p

The defining if expression for the odd prime discriminant.

@[simp]

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_of_mod_four_eq_one {p : ℕ} (hp : p % 4 = 1) : oddPrimeDiscriminant p = ↑p

If p ≡ 1 (mod 4), its odd prime discriminant is p.

@[simp]

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_of_mod_four_ne_one {p : ℕ} (hp : p % 4 ≠ 1) : oddPrimeDiscriminant p = -↑p

If p ≠ 1 (mod 4), its odd prime discriminant is -p. For an odd prime this is the p ≡ 3 (mod 4) case.

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_of_mod_four_eq_three {p : ℕ} (hp : p % 4 = 3) : oddPrimeDiscriminant p = -↑p

If p ≡ 3 (mod 4), its odd prime discriminant is -p.

@[simp]

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_natAbs (p : ℕ) : (oddPrimeDiscriminant p).natAbs = p

The absolute value of the odd prime discriminant is the underlying natural number.

@[simp]

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_ne_zero {p : ℕ} : oddPrimeDiscriminant p ≠ 0 ↔ p ≠ 0

The odd prime discriminant is nonzero exactly when p is nonzero.

theorem TauCeti.Multiquadratic.prime_oddPrimeDiscriminant {p : ℕ} (hp : Nat.Prime p) : Prime (oddPrimeDiscriminant p)

The odd prime discriminant of a natural prime is a prime integer.

theorem TauCeti.Multiquadratic.squarefree_oddPrimeDiscriminant {p : ℕ} (hp : Squarefree p) : Squarefree (oddPrimeDiscriminant p)

The odd prime discriminant of a squarefree natural number is squarefree.

@[simp]

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_dvd_iff {p : ℕ} {D : ℤ} : oddPrimeDiscriminant p ∣ D ↔ ↑p ∣ D

The odd prime discriminant divides an integer exactly when p does.

@[simp]

theorem TauCeti.Multiquadratic.dvd_oddPrimeDiscriminant_iff {p : ℕ} {q : ℤ} : q ∣ oddPrimeDiscriminant p ↔ q ∣ ↑p

An integer divides an odd prime discriminant exactly when it divides the underlying natural number. This form is convenient when checking the unramifiedness side of the splitting law.

theorem TauCeti.Multiquadratic.not_dvd_oddPrimeDiscriminant_iff {p : ℕ} {q : ℤ} : ¬q ∣ oddPrimeDiscriminant p ↔ ¬q ∣ ↑p

An integer does not divide an odd prime discriminant exactly when it does not divide the underlying natural number. The negated form is convenient for the unramifiedness side of the splitting law.

theorem TauCeti.Multiquadratic.forall_not_dvd_oddPrimeDiscriminant_iff {ι : Type u_1} (p : ι → ℕ) {q : ℤ} : (∀ (i : ι), ¬q ∣ oddPrimeDiscriminant (p i)) ↔ ∀ (i : ι), ¬q ∣ ↑(p i)

Family form of unramifiedness for odd prime discriminants: an integer divides none of the p i* exactly when it divides none of the underlying p i.

theorem TauCeti.Multiquadratic.odd_oddPrimeDiscriminant {p : ℕ} (hp : Odd p) : Odd (oddPrimeDiscriminant p)

The odd prime discriminant of an odd natural number is odd.

@[simp]

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_mod_four_eq_one {p : ℕ} (hp : Odd p) : oddPrimeDiscriminant p % 4 = 1

For an odd p, the odd prime discriminant is congruent to 1 modulo 4.

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_eq_or_eq_neg {p : ℕ} : oddPrimeDiscriminant p = ↑p ∨ oddPrimeDiscriminant p = -↑p

The odd prime discriminant is always either p or -p.

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_pos_iff {p : ℕ} : 0 < oddPrimeDiscriminant p ↔ p % 4 = 1

The sign of the odd prime discriminant is controlled by p mod 4.

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_neg_iff {p : ℕ} (hp : Odd p) : oddPrimeDiscriminant p < 0 ↔ p % 4 = 3

The odd prime discriminant is negative exactly in the p ≡ 3 (mod 4) case.

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_eq_neg_one_pow_div_two_mul {p : ℕ} (hp : Odd p) : oddPrimeDiscriminant p = (-1) ^ (p / 2) * ↑p

The odd prime discriminant in the standard notation p* = (-1)^(p/2) p.

theorem TauCeti.Multiquadratic.oddPrimeDiscriminant_eq_neg_one_pow_pred_div_two_mul {p : ℕ} (hp : Odd p) : oddPrimeDiscriminant p = (-1) ^ ((p - 1) / 2) * ↑p

The odd prime discriminant in the standard notation p* = (-1)^((p - 1)/2) p.