structure Hex.RCF.CarrierCert : Type

Multiplication-checkable witnesses that a polynomial is a square-free carrier for the atom product of a sentence.

• carrier : ZPoly

  Proposed square-free carrier P.

• repeated : ZPoly

  Repeated-factor witness R.

• derivPart : ZPoly

  Derivative quotient witness S.

• factorScale : Int

  Nonzero scale k in Q = scale k (P * R).

• derivScale : Int

  Nonzero scale d in scale d Q' = R * S.

• replay : SturmReplay

  Generalized Sturm replay proving the carrier squarefree.

def Hex.RCF.CarrierCert.check (s : Sentence) (cert : CarrierCert) : Bool

Executable carrier validation. The atom product is recomputed from the sentence and is never supplied by the certificate.

Equations

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

def Hex.RCF.CarrierCert.Valid (s : Sentence) (cert : CarrierCert) : Prop

Proposition-level facts recovered from the Boolean carrier checker.

Equations

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

theorem Hex.RCF.CarrierCert.check_sound {s : Sentence} {cert : CarrierCert} (h : check s cert = true) : Valid s cert

Soundness of the executable carrier checker.

theorem Hex.RCF.CarrierCert.replay_of_check {s : Sentence} {cert : CarrierCert} (h : check s cert = true) : SturmReplay.check cert.carrier cert.replay = true

The carrier replay component recovered from the combined checker.

theorem Hex.RCF.CarrierCert.carrier_ne_zero {s : Sentence} {cert : CarrierCert} (h : check s cert = true) : cert.carrier ≠ 0

An accepted carrier certificate has a nonzero carrier polynomial.

theorem Hex.RCF.CarrierCert.product_ne_zero {s : Sentence} {cert : CarrierCert} (h : check s cert = true) : s.product ≠ 0

The recomputed atom product is nonzero for an accepted certificate.