def HexBerlekampZassenhausTheory.CertificateReplay.checkProof (check : Lean.Expr) : Lean.MetaM Lean.Expr

Prove a literal Boolean certificate check by theorem-backed evaluation. Uses direct reduction when available, otherwise public reduction equations. Returns an ordinary kernel proof of check = true, rejecting false or stuck checks. The caller supplies the existing checker applied to reified data.

Equations

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

theorem HexBerlekampZassenhausTheory.CertificateReplay.checkCover (factors : List Hex.ZPoly) (certified : List (Hex.ZPoly × Hex.ZPoly.IrredWitness)) (multiPrime : List (Hex.ZPoly × Hex.ZPolyIrreducibilityCertificate)) (hcert : (certified.all fun (e : Hex.ZPoly × Hex.ZPoly.IrredWitness) => e.1.checkIrredWitness e.2) = true) (hmulti : (multiPrime.all fun (e : Hex.ZPoly × Hex.ZPolyIrreducibilityCertificate) => checkMultiPrimeCert e.1 e.2) = true) (hcover : (factors.all fun (q : Hex.ZPoly) => (certified.any fun (e : Hex.ZPoly × Hex.ZPoly.IrredWitness) => Hex.DensePoly.beqCoeffs e.1 q) || multiPrime.any fun (e : Hex.ZPoly × Hex.ZPolyIrreducibilityCertificate) => Hex.DensePoly.beqCoeffs e.1 q) = true) : checkMultiPrimeCover factors certified multiPrime = true

Assemble the existing cover checker from its three Boolean checks. Only the multi-prime check needs theorem-backed evaluation; the free witness and coefficientwise membership checks retain direct kernel reduction.