Documentation

LeanPool.MarkoffModP.BGS.Markoff.Opening.CyclotomicBound

The concrete cyclotomic opening bound #

This file evaluates the integral cyclotomic defect at the compatible residue prime and connects that vanishing to the archimedean norm estimate.

source
noncomputable def BGS.Markoff.openingCyclotomicIntegerTrace (n a : ℕ) [NeZero n] :
OpeningCyclotomicIntegers n

An integral reciprocal trace, written polynomially using ζⁿ = 1.

Equations
Instances For
    source
    noncomputable def BGS.Markoff.openingCyclotomicIntegerDefect (n a₁ a₂ a₃ : ℕ) [NeZero n] :
    OpeningCyclotomicIntegers n

    The integral defect formed from three polynomial reciprocal traces.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGS.Markoff.coe_openingCyclotomicIntegerTrace (n a : ℕ) [NeZero n] (ha : a ≤ n) :
      ↑(openingCyclotomicIntegerTrace n a) = cyclotomicTrace (openingCyclotomicRoot n ^ a)

      Coercing the integral polynomial trace to the cyclotomic field gives the reciprocal trace.

      source
      theorem BGS.Markoff.coe_openingCyclotomicIntegerDefect (n a₁ a₂ a₃ : ℕ) [NeZero n] (ha₁ : a₁ ≤ n) (ha₂ : a₂ ≤ n) (ha₃ : a₃ ≤ n) :
      ↑(openingCyclotomicIntegerDefect n a₁ a₂ a₃) = cyclotomicDefect (openingCyclotomicRoot n ^ a₁) (openingCyclotomicRoot n ^ a₂) (openingCyclotomicRoot n ^ a₃)

      Coercing the integral polynomial defect gives the characteristic-zero cyclotomic defect.

      source
      theorem BGS.Markoff.openingCyclotomicReduction_integerTrace (p n a : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) (ha : a ≤ n) :
      (openingCyclotomicReduction p n hcoprime ω hω) (openingCyclotomicIntegerTrace n a) = cyclotomicTrace (ω ^ a)

      Compatible reduction sends the polynomial integral trace to the prescribed residue trace.

      source
      theorem BGS.Markoff.openingCyclotomicReduction_integerDefect (p n a₁ a₂ a₃ : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) (ha₁ : a₁ ≤ n) (ha₂ : a₂ ≤ n) (ha₃ : a₃ ≤ n) :
      (openingCyclotomicReduction p n hcoprime ω hω) (openingCyclotomicIntegerDefect n a₁ a₂ a₃) = cyclotomicDefect (ω ^ a₁) (ω ^ a₂) (ω ^ a₃)

      Compatible reduction sends the integral defect to the residue-field cyclotomic defect.

      source
      theorem BGS.Markoff.residueCyclotomicDefect_eq_zero_of_normalizedMarkoff {p : ℕ} [Fact (Nat.Prime p)] (x : NormalizedPoint (OpeningResidueClosure p)) (hx : IsNormalizedMarkoff x) {z₁ z₂ z₃ : OpeningResidueClosure p} (h₁ : x.u1 = cyclotomicTrace z₁) (h₂ : x.u2 = cyclotomicTrace z₂) (h₃ : x.u3 = cyclotomicTrace z₃) :
      cyclotomicDefect z₁ z₂ z₃ = 0

      A normalized residue Markoff point makes the corresponding residue cyclotomic defect vanish.

      source
      theorem BGS.Markoff.openingCyclotomicIntegerDefect_mem_prime_of_normalizedMarkoff (p n a₁ a₂ a₃ : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) (ha₁ : a₁ ≤ n) (ha₂ : a₂ ≤ n) (ha₃ : a₃ ≤ n) (x : NormalizedPoint (OpeningResidueClosure p)) (hx : IsNormalizedMarkoff x) (h₁ : x.u1 = cyclotomicTrace (ω ^ a₁)) (h₂ : x.u2 = cyclotomicTrace (ω ^ a₂)) (h₃ : x.u3 = cyclotomicTrace (ω ^ a₃)) :
      openingCyclotomicIntegerDefect n a₁ a₂ a₃ ∈ openingCyclotomicPrime p n hcoprime ω hω

      The integral defect therefore belongs to the compatible prime selected by the residue root.

      source
      theorem BGS.Markoff.openingCyclotomicDefect_ne_zero_of_residuePoint_ne_origin (p n a₁ a₂ a₃ : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) (ha₁ : a₁ ≤ n) (ha₂ : a₂ ≤ n) (ha₃ : a₃ ≤ n) (x : NormalizedPoint (OpeningResidueClosure p)) (h₁ : x.u1 = cyclotomicTrace (ω ^ a₁)) (h₂ : x.u2 = cyclotomicTrace (ω ^ a₂)) (h₃ : x.u3 = cyclotomicTrace (ω ^ a₃)) (hxne : x ≠ normalizedOrigin) :
      cyclotomicDefect (openingCyclotomicRoot n ^ a₁) (openingCyclotomicRoot n ^ a₂) (openingCyclotomicRoot n ^ a₃) ≠ 0

      If the residue traces form a nonorigin point, the characteristic-zero cyclotomic defect of the compatible powers is nonzero.

      source
      theorem BGS.Markoff.modulus_le_twenty_pow_totient_of_compatible_residue_traces (p n a₁ a₂ a₃ : ℕ) [Fact (Nat.Prime p)] [NeZero n] (hcoprime : p.Coprime n) (ω : OpeningResidueClosure p) (hω : IsPrimitiveRoot ω n) (ha₁ : a₁ ≤ n) (ha₂ : a₂ ≤ n) (ha₃ : a₃ ≤ n) (x : NormalizedPoint (OpeningResidueClosure p)) (hx : IsNormalizedMarkoff x) (h₁ : x.u1 = cyclotomicTrace (ω ^ a₁)) (h₂ : x.u2 = cyclotomicTrace (ω ^ a₂)) (h₃ : x.u3 = cyclotomicTrace (ω ^ a₃)) (hxne : x ≠ normalizedOrigin) :
      p ≤ 20 ^ n.totient

      The concrete cyclotomic opening inequality. A nonorigin normalized Markoff point whose three coordinates are reciprocal traces of powers of one primitive residue root forces p ≤ 20 ^ φ(n).