Documentation

LeanPool.MarkoffModP.BGS.Markoff.Core.TraceClassification

Split and nonsplit trace classification #

This module proves the elementary representation of every normalized trace over an odd prime field by either the split torus or the concrete norm-one torus in the canonical quadratic extension.

source
theorem BGS.Markoff.isSquare_algebraMap_quadraticFiniteField (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (a : ZMod p) :
IsSquare ((algebraMap (ZMod p) (quadraticFiniteField p)) a)

Every base-field scalar becomes a square in the canonical quadratic extension.

source
theorem BGS.Markoff.exists_split_or_quadraticNormOneTrace (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) :
(∃ (w : (ZMod p)ˣ), splitTorusTrace w = t ∧ ↑w ^ 2 ≠ 1) ∨ ∃ (w : ↥(quadraticNormOneTorus p)), quadraticNormOneTrace p w = t ∧ ↑↑w ^ 2 ≠ 1

Every nonparabolic normalized trace over an odd prime field is represented by either the split torus or the concrete norm-one torus in the canonical quadratic extension.

source
def BGS.Markoff.normalizedParabolicTraceSet (p : ℕ) [Fact (Nat.Prime p)] :
Finset (ZMod p)

The two normalized parabolic trace parameters.

Equations
Instances For
    source
    noncomputable def BGS.Markoff.concreteLowOrderTraceSet (p : ℕ) [Fact (Nat.Prime p)] (bound : ℕ) :
    Finset (ZMod p)

    The concrete low-order trace set used for normalized Markoff rotations over ZMod p.

    Equations
    Instances For
      source
      theorem BGS.Markoff.concreteLowOrderTraceSet_card_le (p : ℕ) [Fact (Nat.Prime p)] (bound : ℕ) :
      (concreteLowOrderTraceSet p bound).card ≤ 2 + 2 * bound ^ 2

      The concrete trace set has the quadratic cardinality bound needed in the giant-orbit count.

      source
      theorem BGS.Markoff.mem_concreteLowOrderTraceSet_of_rotationOrder_lt (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (bound : ℕ) (hsmall : rotationOrder t < bound) :
      t ∈ concreteLowOrderTraceSet p bound

      A normalized trace of small rotation order lies in the concrete union of the parabolic, split-torus, and quadratic norm-one bounded-order trace sets.