Documentation

MazurTorsion.NumberTheory.CyclotomicStickelbergerTwo

The corrected b = 2 Stickelberger coefficient #

This file isolates the elementary finite arithmetic behind the b = 2 integral Stickelberger element. For a nonzero residue a modulo an odd prime p, its corrected coefficient is

floor (2 * a.val / p).

It is the indicator of the upper half of the nonzero residues. The corresponding weighted scalar is invertible modulo every prime p ≥ 5; more precisely, eight times that scalar is one.

source
def NumberTheory.CyclotomicCharacter.stickelbergerTwoCoefficient (p : ℕ) (a : (ZMod p)ˣ) :
ℕ

The nonnegative coefficient of σₐ⁻¹ in the negative of the corrected b = 2 Stickelberger element.

Equations
Instances For
    source
    theorem NumberTheory.CyclotomicCharacter.stickelbergerTwoCoefficient_eq_ite {p : ℕ} [Fact (Nat.Prime p)] (a : (ZMod p)ˣ) :
    stickelbergerTwoCoefficient p a = if p ≤ 2 * (↑a).val then 1 else 0

    The corrected b = 2 coefficient is the upper-half indicator.

    source
    theorem NumberTheory.CyclotomicCharacter.stickelbergerTwoCoefficient_eq_zero {p : ℕ} [Fact (Nat.Prime p)] (a : (ZMod p)ˣ) (ha : 2 * (↑a).val < p) :
    stickelbergerTwoCoefficient p a = 0

    Below the upper half, the corrected coefficient vanishes.

    source
    theorem NumberTheory.CyclotomicCharacter.stickelbergerTwoCoefficient_eq_one {p : ℕ} [Fact (Nat.Prime p)] (a : (ZMod p)ˣ) (ha : p ≤ 2 * (↑a).val) :
    stickelbergerTwoCoefficient p a = 1

    On the upper half, the corrected coefficient is one.

    source
    def NumberTheory.CyclotomicCharacter.stickelbergerTwoWeightedScalar (p : ℕ) [NeZero p] :
    ZMod p

    The weighted scalar through which the corrected b = 2 element acts on the inverse-character component.

    Equations
    Instances For
      source
      theorem NumberTheory.CyclotomicCharacter.stickelbergerTwoWeightedScalar_eq_upperHalfSum {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) :
      stickelbergerTwoWeightedScalar p = ∑ n ∈ Finset.Icc (p / 2 + 1) (p - 1), ↑n

      Reindexing by least positive representatives turns the weighted scalar into the sum of the upper-half representatives.

      source
      theorem NumberTheory.CyclotomicCharacter.eight_mul_sum_upperHalf {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) :
      8 * ∑ n ∈ Finset.Icc (p / 2 + 1) (p - 1), n = (p - 1) * (3 * p - 1)

      Closed natural-number formula for the upper-half interval. The division-free form is convenient for reduction modulo p.

      source
      theorem NumberTheory.CyclotomicCharacter.eight_mul_upperHalfSum {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) :
      8 * ∑ n ∈ Finset.Icc (p / 2 + 1) (p - 1), ↑n = 1

      Eight times the upper-half sum is one modulo p.

      source
      theorem NumberTheory.CyclotomicCharacter.eight_mul_stickelbergerTwoWeightedScalar {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) :
      8 * stickelbergerTwoWeightedScalar p = 1

      The exact inverse-character scalar identity for the corrected b = 2 coefficient.

      source
      theorem NumberTheory.CyclotomicCharacter.isUnit_stickelbergerTwoWeightedScalar {p : ℕ} [Fact (Nat.Prime p)] (hp5 : 5 ≤ p) :
      IsUnit (stickelbergerTwoWeightedScalar p)

      The corrected b = 2 weighted scalar is a unit modulo p.