def Hex.Berlekamp.checkMonicCert {p : Nat} [ZMod64.Bounds p] (m : FpPoly p) (cert : IrreducibilityCertificate) : Bool

Monic-guarded wrapper around the incremental linear certificate checker: true only when m is monic and the certificate replays. Folding the monicity guard into the Boolean lets reified applications avoid constructing a DensePoly.Monic proof term.

Equations

• Hex.Berlekamp.checkMonicCert m cert = if hmonic : Hex.DensePoly.leadingCoeff m = 1 then Hex.Berlekamp.checkIrreducibilityCertificateLinearIncremental m hmonic cert else false

theorem Hex.Berlekamp.irreducible_of_checkMonicCert {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (m : FpPoly p) (cert : IrreducibilityCertificate) (hcheck : checkMonicCert m cert = true) : m.Irreducible

A passing checkMonicCert forces irreducibility of the (necessarily monic) input.

theorem Hex.Berlekamp.irreducible_of_checkMonicCert_scale {p : Nat} [ZMod64.Bounds p] (f m : FpPoly p) (c : ZMod64 p) (cert : IrreducibilityCertificate) (hp : Nat.isPrimeTrial p = true) (hc : decide (c = 0) = false) (hfm : (DensePoly.scale c m).beqCoeffs f = true) (hcheck : checkMonicCert m cert = true) : f.Irreducible

Kernel-decidable irreducibility for a possibly non-monic f : FpPoly p: f reconstructs as scale c m for a monic m whose Rabin certificate replays, with a nonzero scalar and a prime modulus. Every hypothesis is a Boolean check on literal data.

def Hex.Berlekamp.checkIrredCover {p : Nat} [ZMod64.Bounds p] (factors : List (FpPoly p)) (certified : List (FpPoly p × ZMod64 p × IrreducibilityCertificate)) : Bool

Bulk kernel-decidable irreducibility for a factor list with repetition: certified carries one (monic, scalar, certificate) entry per distinct factor, and every listed factor must match some entry's scale scalar monic by beqCoeffs. Each certificate is replayed once regardless of multiplicity; repeated factors cost only a coefficient comparison.

Equations

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

theorem Hex.Berlekamp.irreducible_of_checkIrredCover {p : Nat} [ZMod64.Bounds p] (hp : Nat.isPrimeTrial p = true) (factors : List (FpPoly p)) (certified : List (FpPoly p × ZMod64 p × IrreducibilityCertificate)) (hcheck : checkIrredCover factors certified = true) (q : FpPoly p) : q ∈ factors → q.Irreducible

A passing checkIrredCover forces irreducibility of every listed factor. The single Boolean hypothesis is the factors_irred slot of a reified FpPoly.Factored value.