theorem Hex.RCF.CommonRootCert.isRoot_iff {atom carrier : ZPoly} {cert : CommonRootCert} (h : check atom carrier cert = true) (x : ℝ) : (HexRealRootsMathlib.toPolyℝ cert.gcd).IsRoot x ↔ (HexRealRootsMathlib.toPolyℝ atom).IsRoot x ∧ (HexRealRootsMathlib.toPolyℝ carrier).IsRoot x

A checked common-root polynomial has exactly the common real roots of the atom and carrier.

theorem Hex.RCF.CommonRootCert.noRoot_of_constant {atom carrier : ZPoly} {cert : CommonRootCert} (h : check atom carrier cert = true) (hreplay : cert.replay = none) (x : ℝ) : ¬(HexRealRootsMathlib.toPolyℝ cert.gcd).IsRoot x

A checked constant common-root branch has no real roots.

theorem Hex.RCF.CommonRootCert.count_eq_one_iff {carrier : ZPoly} {carrierReplay : SturmReplay} (hcarrier : SturmReplay.check carrier carrierReplay = true) {isolations : IsolationCert} (hcert : IsolationCert.check carrierReplay isolations = true) {atom : ZPoly} {common : CommonRootCert} {gcdReplay : SturmReplay} (hcommon : check atom carrier common = true) (hgcdReplay : common.replay = some gcdReplay) (i : Fin isolations.intervals.size) {root : ℝ} (hroot : (HexRealRootsMathlib.toPolyℝ carrier).IsRoot root) (hmem : HexRealRootsMathlib.Literal.InInterval isolations.intervals[i] root) : gcdReplay.count isolations.intervals[i] = 1 ↔ (HexRealRootsMathlib.toPolyℝ atom).IsRoot root

A cached nonconstant replay counts one common root in a carrier isolation exactly when the atom vanishes at its supplied carrier root.

theorem Hex.RCF.CommonRootCert.hasRoot_iff {carrier : ZPoly} {carrierReplay : SturmReplay} (hcarrier : SturmReplay.check carrier carrierReplay = true) {isolations : IsolationCert} (hcert : IsolationCert.check carrierReplay isolations = true) {atom : ZPoly} {common : CommonRootCert} (hcommon : check atom carrier common = true) (i : Fin isolations.intervals.size) {root : ℝ} (hroot : (HexRealRootsMathlib.toPolyℝ carrier).IsRoot root) (hmem : HexRealRootsMathlib.Literal.InInterval isolations.intervals[i] root) : common.hasRoot isolations.intervals[i] = true ↔ (HexRealRootsMathlib.toPolyℝ atom).IsRoot root

The executable cached-root query is exact at a supplied carrier root in a checked isolation, including the constant-gcd branch.

theorem Hex.RCF.CommonRootCert.hasRoot_model_iff {carrier : ZPoly} {carrierReplay : SturmReplay} (hcarrier : SturmReplay.check carrier carrierReplay = true) {isolations : IsolationCert} (hstrict : IsolationCert.checkStrict carrierReplay isolations = true) {atom : ZPoly} {common : CommonRootCert} (hcommon : check atom carrier common = true) (i : Fin isolations.intervals.size) : common.hasRoot isolations.intervals[i] = true ↔ (HexRealRootsMathlib.toPolyℝ atom).IsRoot ((isolations.rootModel hcarrier hstrict).root i)

Specialize hasRoot_iff to the canonical root model of a strict isolation certificate.