structure Hex.RCF.CommonRootCert : Type

Multiplication-checkable witnesses for the common roots of an atom and a carrier polynomial. The atom and carrier themselves are external checker inputs, so certificate data cannot silently substitute different polynomials.

• gcd : ZPoly

  Proposed common-root polynomial.

• atomFactor : ZPoly

  Quotient witnessing that the common-root polynomial divides the atom.

• carrierFactor : ZPoly

  Quotient witnessing that the common-root polynomial divides the carrier.

• atomCoeff : ZPoly

  Atom coefficient in the scaled Bezout identity.

• carrierCoeff : ZPoly

  Carrier coefficient in the scaled Bezout identity.

• scale : Int

  Nonzero integer scale in the Bezout identity.

• replay : Option SturmReplay

  Cached replay for a nonconstant common-root polynomial. A nonzero constant common-root polynomial uses none.

def Hex.RCF.CommonRootCert.checkReplay (cert : CommonRootCert) : Bool

Validate the constant/nonconstant replay branch.

Equations

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

def Hex.RCF.CommonRootCert.ReplayValid (cert : CommonRootCert) : Prop

Proposition-level replay facts recovered from checkReplay.

Equations

• cert.ReplayValid = match cert.replay with | none => Hex.DensePoly.size cert.gcd = 1 | some replay => 0 < Hex.DensePoly.natDegree cert.gcd ∧ Hex.RCF.SturmReplay.check cert.gcd replay = true

def Hex.RCF.CommonRootCert.check (atom carrier : ZPoly) (cert : CommonRootCert) : Bool

Check the divisibility and scaled Bezout identities against the external atom and carrier polynomials.

Equations

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

def Hex.RCF.CommonRootCert.Valid (atom carrier : ZPoly) (cert : CommonRootCert) : Prop

Proposition-level facts recovered from the common-root checker.

Equations

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

theorem Hex.RCF.CommonRootCert.checkReplay_sound {cert : CommonRootCert} (h : cert.checkReplay = true) : cert.ReplayValid

Soundness of the constant/nonconstant replay branch.

theorem Hex.RCF.CommonRootCert.check_sound {atom carrier : ZPoly} {cert : CommonRootCert} (h : check atom carrier cert = true) : Valid atom carrier cert

Soundness of the executable common-root checker.

theorem Hex.RCF.CommonRootCert.gcd_ne_zero {atom carrier : ZPoly} {cert : CommonRootCert} (h : check atom carrier cert = true) : cert.gcd ≠ 0

A checked common-root polynomial is nonzero in both certificate branches.

theorem Hex.RCF.CommonRootCert.replay_of_check {atom carrier : ZPoly} {cert : CommonRootCert} {replay : SturmReplay} (h : check atom carrier cert = true) (hreplay : cert.replay = some replay) : SturmReplay.check cert.gcd replay = true

Recover the checked replay in the nonconstant certificate branch.

def Hex.RCF.CommonRootCert.hasRoot (cert : CommonRootCert) (I : DyadicInterval) : Bool

Decide whether the cached common-root polynomial has a root in an interval. The constant branch is root-free. The nonconstant branch reads its shared generalized Sturm replay.

Equations

• cert.hasRoot I = match cert.replay with | none => false | some replay => decide (replay.count I = 1)