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

Kernel-replayable modular composition using structural Horner evaluation.

Equations

• Hex.Conway.compose f g modulus hm = g.composeModMonicList modulus hm (Hex.DensePoly.toArray f).toList

theorem Hex.Conway.compose_eq {p : Nat} [ZMod64.Bounds p] (f g modulus : FpPoly p) (hm : DensePoly.Monic modulus) : compose f g modulus hm = f.composeModMonicImpl g modulus hm

Structural composition agrees with the compiled packed dispatcher.

@[csimp]

theorem Hex.Conway.compose_eq_impl : @compose = @FpPoly.composeModMonicImpl

Preserve the optimized implementation in compiled clients.

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

Structural square-and-multiply. Fuel bounds the number of steps; the exponent is halved at each step. No well-founded recursion is replayed.

Equations

• Hex.Conway.powAux f hm 0 x✝² x✝¹ x✝ = x✝
• Hex.Conway.powAux f hm n.succ 0 x✝¹ x✝ = x✝
• Hex.Conway.powAux f hm fuel.succ n.succ x✝¹ x✝ = Hex.Conway.powAux f hm fuel ((n + 1) / 2) (f.modByMonic (x✝¹ * x✝¹) hm) (if (n + 1) % 2 = 0 then x✝ else f.modByMonic (x✝ * x✝¹) hm)

theorem Hex.Conway.powAux_eq {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hm : DensePoly.Monic f) (fuel n : Nat) (base acc : FpPoly p) (h : n ≤ fuel) : powAux f hm fuel n base acc = f.powModMonicAux hm n base acc

With sufficient fuel, structural replay agrees with executable modular power.

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

Kernel-replayable binary modular power. The exponent itself is a conservative fuel bound; only logarithmically many steps are evaluated.

Equations

• Hex.Conway.powMod base f hm n = Hex.Conway.powAux f hm n n (f.modByMonic base hm) 1

theorem Hex.Conway.powMod_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (base f : FpPoly p) (hm : DensePoly.Monic f) (n : Nat) : powMod base f hm n = base.powModMonicLinear f hm n

Structural binary power computes the same residue as linear power.

def Hex.Conway.checkStep {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hm : DensePoly.Monic f) (cert : Berlekamp.SamePrimeIrreducibilityCertificate p) (k : Nat) : Bool

One Frobenius step checked by structural binary exponentiation.

Equations

• Hex.Conway.checkStep f hm cert k = match cert.powChain[k]?, cert.powChain[k + 1]? with | some prev, some next => next == Hex.Conway.powMod prev f hm p | x, x_1 => false

def Hex.Conway.checkChain {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hm : DensePoly.Monic f) (cert : Berlekamp.SamePrimeIrreducibilityCertificate p) : Bool

Binary replay of the committed Frobenius chain.

Equations

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

def Hex.Conway.checkRabin {p : Nat} [ZMod64.Bounds p] (f : FpPoly p) (hm : DensePoly.Monic f) (cert : Berlekamp.IrreducibilityCertificate) : Bool

Rabin certificate replay using binary modular powers. The certificate shape and every check other than the power implementation are unchanged.

Equations

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

theorem Hex.Conway.checkRabin_eq {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (f : FpPoly p) (hm : DensePoly.Monic f) (cert : Berlekamp.IrreducibilityCertificate) : checkRabin f hm cert = Berlekamp.checkIrreducibilityCertificateLinearIncremental f hm cert

Binary replay preserves the existing Rabin checker exactly.