def Hex.Conway.linPowMod {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hm : DensePoly.Monic f) (x : FpPoly p) : Nat → FpPoly p

Structural modular power: k multiplications, each followed by reduction. A proof helper for induction; executable certificate replay uses powMod.

Equations

• Hex.Conway.linPowMod f hm x 0 = 1
• Hex.Conway.linPowMod f hm x k.succ = f.modByMonic (Hex.Conway.linPowMod f hm x k * x) hm

theorem Hex.Conway.linPowMod_eq {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hm : DensePoly.Monic f) (x : FpPoly p) (k : Nat) : linPowMod f hm x k = x.powModMonicLinear f hm k

The structural linear helper agrees with the polynomial library's power.

def Hex.Conway.powerResidue {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hm : DensePoly.Monic f) (k : Nat) : FpPoly p

A reduced representative of the generator raised to a supplied exponent.

Equations

• Hex.Conway.powerResidue f hm k = f.modByMonic (Hex.Conway.powMod Hex.FpPoly.X f hm k) hm

def Hex.Conway.primePowerProduct : List Nat → List Nat → Nat

The product of qs raised to the matching multiplicities in es.

Equations

• Hex.Conway.primePowerProduct [] x✝ = 1
• Hex.Conway.primePowerProduct x✝ [] = 1
• Hex.Conway.primePowerProduct (q :: qs) (e :: es) = q ^ e * Hex.Conway.primePowerProduct qs es

def Hex.Conway.primitiveCheck {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hm : DensePoly.Monic f) (n : Nat) (qs es : List Nat) : Bool

The Tier 2 primitivity check validates the factorization of p^n - 1 and checks the full power and each prime-divided power. Primality of the supplied factors is carried separately by Primitive.

Equations

• One or more equations did not get rendered due to their size.

structure Hex.Conway.Primitive (p n : Nat) [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (h : SupportedEntry p n) (qs es : List Nat) : Prop

The committed entry C(p, n) is primitive: the residue of x has multiplicative order exactly p^n - 1, witnessed by the supplied factorization and power data.

• primes (q : Nat) : q ∈ qs → Nat.Prime q

  The supplied divisors are prime. Together with the product check inside primitiveCheck this ensures they include every prime divisor of p^n - 1.

• check : primitiveCheck (conwayPoly p n h) ⋯ n qs es = true

  The arithmetic and the two power conditions, all decidable.