theorem Hex.RCF.CarrierCert.squarefree {s : Sentence} {cert : CarrierCert} (h : check s cert = true) : Squarefree (HexRealRootsMathlib.toPolyℝ cert.carrier)

An accepted carrier is squarefree after casting to real coefficients.

theorem Hex.RCF.CarrierCert.isRoot_factor_iff {q p r t : ZPoly} {k d : ℤ} (hq0 : q ≠ 0) (hk0 : k ≠ 0) (hd0 : d ≠ 0) (hfactorZ : q = DensePoly.scale k (p * r)) (hderivZ : DensePoly.scale d (DensePoly.derivative q) = r * t) (x : ℝ) : (HexRealRootsMathlib.toPolyℝ p).IsRoot x ↔ (HexRealRootsMathlib.toPolyℝ q).IsRoot x

Exact scalar-and-factor identities imply that the proposed factor and the original polynomial have the same real roots.

theorem Hex.RCF.CarrierCert.isRoot_carrier_iff_product {s : Sentence} {cert : CarrierCert} (h : check s cert = true) (x : ℝ) : (HexRealRootsMathlib.toPolyℝ cert.carrier).IsRoot x ↔ (HexRealRootsMathlib.toPolyℝ s.product).IsRoot x

Exact identities accepted by the checker imply that the carrier and recomputed atom product have the same real roots.

theorem Hex.RCF.isRoot_prod_iff {ps : List ZPoly} (x : ℝ) : (HexRealRootsMathlib.toPolyℝ ps.prod).IsRoot x ↔ ∃ p ∈ ps, (HexRealRootsMathlib.toPolyℝ p).IsRoot x

A real root of a product of literal integer polynomials is exactly a root of one list member.

theorem Hex.RCF.CarrierCert.isRoot_iff_atom {s : Sentence} {cert : CarrierCert} (h : check s cert = true) (x : ℝ) : (HexRealRootsMathlib.toPolyℝ cert.carrier).IsRoot x ↔ ∃ p ∈ s.polys, (HexRealRootsMathlib.toPolyℝ p).IsRoot x

The accepted carrier roots are exactly the union of the roots of the nonconstant atom polynomials recomputed from the sentence.