theorem HexRealRootsMathlib.degree_pos_of_count_one {p : Hex.ZPoly} (iso : Hex.RealRootIsolation p) : 1 ≤ Hex.DensePoly.natDegree p

A Sturm count of 1 forces positive degree: a degree-≤ 0 input has the empty chain, whose count is 0 at every pair of endpoints.

theorem HexRealRootsMathlib.degree?_ne_none {p : Hex.ZPoly} (hp0 : p ≠ 0) : Hex.DensePoly.degree? p ≠ none

A nonzero executable polynomial has a some degree: degree? = none means zero stored size, which pins every coefficient (hence the polynomial) to zero.

theorem HexRealRootsMathlib.RealRootIsolation.exists_unique_root {p : Hex.ZPoly} (hp : p.SquareFreeRat) (iso : Hex.RealRootIsolation p) : ∃! r : ℝ, (toPolyℝ p).IsRoot r ∧ Dyadic.toReal iso.interval.lower < r ∧ r ≤ Dyadic.toReal iso.interval.upper

Isolation soundness. A certified isolation of p names exactly one real root of toPolyℝ p in its half-open interval (lower, upper].

theorem HexRealRootsMathlib.RealRootIsolations.isolates {p : Hex.ZPoly} (hp0 : p ≠ 0) (hp : p.SquareFreeRat) (out : Hex.RealRootIsolations p) (r : ℝ) : (toPolyℝ p).IsRoot r → ∃! iso : Hex.RealRootIsolation p, iso ∈ out.isolations.toList ∧ Dyadic.toReal iso.interval.lower < r ∧ r ≤ Dyadic.toReal iso.interval.upper

Completeness of a run. A complete isolation run of a nonzero, rationally squarefree p names every real root of toPolyℝ p exactly once: each root lies in exactly one of the emitted half-open intervals.

The SquareFreeRat p hypothesis alone is insufficient: for p = 0 (which passes SquareFreeRat) every real is a root while complete forces zero isolations, so no root is captured. p ≠ 0 is the honest hypothesis: a nonzero constant has no roots (vacuous case), and the positive-degree case is isolates_of_degree_pos.

theorem Hex.RealRootIsolation.exists_unique_root {p : ZPoly} (hp : p.SquareFreeRat) (iso : RealRootIsolation p) : ∃! r : ℝ, (HexRealRootsMathlib.toPolyℝ p).IsRoot r ∧ HexRealRootsMathlib.Dyadic.toReal iso.interval.lower < r ∧ r ≤ HexRealRootsMathlib.Dyadic.toReal iso.interval.upper

Dot-notation alias in the Hex namespace for HexRealRootsMathlib.RealRootIsolation.exists_unique_root, so iso.exists_unique_root resolves directly on a Hex.RealRootIsolation.

theorem Hex.RealRootIsolations.isolates {p : ZPoly} (hp0 : p ≠ 0) (hp : p.SquareFreeRat) (out : RealRootIsolations p) (r : ℝ) : (HexRealRootsMathlib.toPolyℝ p).IsRoot r → ∃! iso : RealRootIsolation p, iso ∈ out.isolations.toList ∧ HexRealRootsMathlib.Dyadic.toReal iso.interval.lower < r ∧ r ≤ HexRealRootsMathlib.Dyadic.toReal iso.interval.upper

Dot-notation alias in the Hex namespace for HexRealRootsMathlib.RealRootIsolations.isolates, so out.isolates resolves directly on a Hex.RealRootIsolations.