theorem Hex.CertificateSyntax.boundsOfDecide (p : Nat) (h : (decide (0 < p) && decide (p < 2 ^ 31)) = true) : ZMod64.Bounds p

Rebuild a ZMod64.Bounds instance from a single kernel-decidable Boolean check. The reifier emits boundsOfDecide p (Eq.refl true) in every reified instance slot, so the kernel discharges both bounds by reduction.

def Hex.CertificateSyntax.reflTrue : Lean.Expr

The literal proof Eq.refl true, accepted in any b = true slot whose left-hand side the kernel can reduce to true.

Equations

• Hex.CertificateSyntax.reflTrue = Lean.mkApp2 (Lean.mkConst `Eq.refl [Lean.Level.one]) (Lean.mkConst `Bool) (Lean.mkConst `Bool.true)

def Hex.CertificateSyntax.reflFalse : Lean.Expr

The literal proof Eq.refl false, accepted in any b = false slot whose left-hand side the kernel can reduce to false.

Equations

• Hex.CertificateSyntax.reflFalse = Lean.mkApp2 (Lean.mkConst `Eq.refl [Lean.Level.one]) (Lean.mkConst `Bool) (Lean.mkConst `Bool.false)

def Hex.CertificateSyntax.arrayLit (ty : Lean.Expr) (xs : List Lean.Expr) : Lean.Expr

Literal Array expression (List.toArray [x₁, …, xₙ] : Array ty).

Equations

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

def Hex.CertificateSyntax.reifyBounds (pE : Lean.Expr) : Lean.Expr

Reified ZMod64.Bounds p instance: boundsOfDecide p (Eq.refl true).

Equations

• Hex.CertificateSyntax.reifyBounds pE = Lean.mkApp2 (Lean.mkConst `Hex.CertificateSyntax.boundsOfDecide) pE Hex.CertificateSyntax.reflTrue

def Hex.CertificateSyntax.zmodType (pE boundsE : Lean.Expr) : Lean.Expr

The type Hex.ZMod64 p at a reified prime and bounds instance.

Equations

• Hex.CertificateSyntax.zmodType pE boundsE = Lean.mkApp2 (Lean.mkConst `Hex.ZMod64) pE boundsE

def Hex.CertificateSyntax.fpPolyType (pE boundsE : Lean.Expr) : Lean.Expr

The type Hex.FpPoly p at a reified prime and bounds instance.

Equations

• Hex.CertificateSyntax.fpPolyType pE boundsE = Lean.mkApp2 (Lean.mkConst `Hex.FpPoly) pE boundsE

def Hex.CertificateSyntax.reifyZMod64 (pE boundsE : Lean.Expr) (n : Nat) : Lean.Expr

Reify a ZMod64 p residue from its canonical Nat representative as Hex.ZMod64.ofNat p n.

Equations

• Hex.CertificateSyntax.reifyZMod64 pE boundsE n = Lean.mkApp3 (Lean.mkConst `Hex.ZMod64.ofNat) pE (Lean.mkNatLit n) boundsE

def Hex.CertificateSyntax.reifyFpPolyOfNats (pE boundsE : Lean.Expr) (coeffs : List Nat) : Lean.Expr

Reify an FpPoly p from the canonical Nat representatives of its coefficients as Hex.FpPoly.ofCoeffs #[…].

Equations

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

def Hex.CertificateSyntax.fpCoeffNats {p : Nat} [ZMod64.Bounds p] (g : FpPoly p) : List Nat

Canonical Nat representatives of an FpPoly p's coefficient array.

Equations

• Hex.CertificateSyntax.fpCoeffNats g = List.map Hex.ZMod64.toNat (Hex.DensePoly.toArray g).toList

def Hex.CertificateSyntax.reifyRabinWitness {p : Nat} [bounds : ZMod64.Bounds p] (pE boundsE : Lean.Expr) (w : Berlekamp.RabinBezoutWitness p) : Lean.Expr

Reify a RabinBezoutWitness p as a constructor application over reified FpPoly values.

Equations

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

def Hex.CertificateSyntax.reifyRabinCert (cert : Berlekamp.IrreducibilityCertificate) : Lean.Expr

Reify a nested Rabin IrreducibilityCertificate as a constructor application over its reified prime, pow chain, and Bezout witnesses.

Equations

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

def Hex.CertificateSyntax.rabinCertData (cert : Berlekamp.IrreducibilityCertificate) : Nat × Nat × List (List Nat) × List (List Nat × List Nat)

Serialized view of a nested Rabin certificate.

Equations

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