theorem HexRealRootsMathlib.refine1_isolates_same {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 ↔ Dyadic.toReal iso.refine1.interval.lower < r ∧ r ≤ Dyadic.toReal iso.refine1.interval.upper)) ∧ Dyadic.toReal iso.refine1.interval.width = Dyadic.toReal iso.interval.width / 2

One refinement step preserves the root and halves the width. For a squarefree p, iso.refine1 isolates the same real root as iso (a root lies in iso's interval iff it lies in the refined interval) and its width is exactly half. The fallback branch of refine1 is never taken: the two half-counts sum to 1, so exactly one half certifies.

theorem HexRealRootsMathlib.neg_rootBound_lt_rootBound (p : Hex.ZPoly) : -Hex.rootBound p < Hex.rootBound p

-rootBound p < rootBound p, so the initial interval is nonempty.

theorem HexRealRootsMathlib.sturmVar_neg_pos_sub {p : Hex.ZPoly} (hdeg : 1 ≤ Hex.DensePoly.natDegree p) (hp : p.SquareFreeRat) : ↑(Hex.sturmVarAt p.sturmChain (-Hex.rootBound p)) - ↑(Hex.sturmVarAt p.sturmChain (Hex.rootBound p)) = ↑p.rootCount

The ±rootBound variation gap equals ZPoly.rootCount. The Sturm variation difference between -rootBound p and rootBound p counts the real roots of p in (-R, R], which is every real root (Cauchy bound), i.e. ZPoly.rootCount p. This is a statement about p's roots only — the chain elements' own (possibly larger) zeros never enter, so there is no ±R-versus-±∞ gap.

theorem HexRealRootsMathlib.initial_width_le (p : Hex.ZPoly) (hdeg : 1 ≤ Hex.DensePoly.natDegree p) : Dyadic.toReal (Hex.rootBound p) - Dyadic.toReal (-Hex.rootBound p) ≤ 2 ^ (↑(Hex.isolationDepth p) - ↑(Hex.sepPrec p))

The initial interval's width fits the depth budget. For positive-degree p, 2 · rootBound p ≤ 2 ^ (isolationDepth p − sepPrec p), which is the depth-sufficiency hypothesis the sturmVisit induction consumes at the top.

theorem HexRealRootsMathlib.dle_refl (a : Dyadic) : a ≤ a

Dyadic ≤ is reflexive (routed through toRat, staying in the core instances that DyadicInterval uses).

theorem HexRealRootsMathlib.dle_of_lt {a b : Dyadic} (h : a < b) : a ≤ b

Dyadic < implies ≤.

theorem HexRealRootsMathlib.dle_trans {a b c : Dyadic} (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c

Transitivity of the core dyadic ≤.

theorem HexRealRootsMathlib.sturmVarAt_le {p : Hex.ZPoly} (hdeg : 1 ≤ Hex.DensePoly.natDegree p) (hp : p.SquareFreeRat) {a b : Dyadic} (hab : a < b) : Hex.sturmVarAt p.sturmChain b ≤ Hex.sturmVarAt p.sturmChain a

sturmVarAt is antitone in the point: the count over (a, b] is a nonnegative cardinality, so the variation at b is at most the one at a.

theorem HexRealRootsMathlib.isRoot_toPolyℂ {p : Hex.ZPoly} {r : ℝ} (hr : (toPolyℝ p).IsRoot r) : (toPolyℂ p).IsRoot ↑r

A real root of the real cast is a complex root of the complex cast.

theorem HexRealRootsMathlib.sturmCount_le_one {p : Hex.ZPoly} (hdeg : 1 ≤ Hex.DensePoly.natDegree p) (hp : p.SquareFreeRat) (J : Hex.DyadicInterval) (hw : Dyadic.toReal J.upper - Dyadic.toReal J.lower ≤ 2 ^ (-↑(Hex.sepPrec p))) : p.sturmCount J ≤ 1

Separation caps the count. An interval no wider than 2^(−sepPrec p) holds at most one real root of a positive-degree squarefree p (two distinct real roots are more than 4·2^(−sepPrec p) apart by sepPrec_separates'), so its exact Sturm count is at most 1.

theorem HexRealRootsMathlib.assemble?_isSome {p : Hex.ZPoly} {chain : Array Hex.ZPoly} (hchain : chain = p.sturmChain) (arr : Array (Hex.RealRootIsolation p)) (hord : ∀ (i j : Fin arr.size), i < j → arr[i].interval.upper ≤ arr[j].interval.lower) (hsize : arr.size = Hex.sturmVarNegInf chain - Hex.sturmVarPosInf chain) : (Hex.assemble? p chain hchain arr).isSome = true

The final assembly step succeeds once its two invariants are witnessed.

theorem HexRealRootsMathlib.isolateSturm?_isSome (p : Hex.ZPoly) (hp0 : p ≠ 0) (hp : p.SquareFreeRat) : p.isolateSturm?.isSome = true

The Sturm engine succeeds on nonzero squarefree input. Positive degree is the real content (isolateSturm?_isSome_of_degree_pos); a nonzero constant certifies through the empty chain.

The p ≠ 0 hypothesis is necessary because SquareFreeRat 0 is vacuous while ZPoly.isolateSturm? 0 = none.

theorem HexRealRootsMathlib.isolateRealRoots?_isSome (p : Hex.ZPoly) (hp0 : p ≠ 0) (hp : p.SquareFreeRat) : p.isolateRealRoots?.isSome = true

The top-level driver succeeds on nonzero squarefree input. A one-liner over isolateSturm?_isSome: ZPoly.isolateRealRoots? keeps whichever engine's certified output arrives first, and the Sturm engine always has one.