theorem HexRealRootsMathlib.bZero_iff {p : Hex.ZPoly} (hi : Dyadic) : (Hex.dyadicSign (p.evalDyadic hi) == 0) = true ↔ (toPolyℝ p).IsRoot (Dyadic.toReal hi)

The executable endpoint test dyadicSign (p(hi)) == 0 decides whether hi is a real root of toPolyℝ p: the exact dyadic evaluation has the same sign as the real evaluation (sign_dyadicSign, toReal_evalDyadic), so it is zero exactly at a root.

theorem HexRealRootsMathlib.descartes_node_count {p : Hex.ZPoly} (hdeg : 1 ≤ Hex.DensePoly.natDegree p) (hp : p.SquareFreeRat) {lo hi : Dyadic} (hlt : lo < hi) : ↑(Hex.sturmVarAt p.sturmChain lo) - ↑(Hex.sturmVarAt p.sturmChain hi) = ↑(Multiset.countP (fun (x : ℝ) => 0 < x) (mobiusPoly (Hex.DensePoly.natDegree p) (Dyadic.toReal lo) (Dyadic.toReal hi) (toPolyℝ p)).roots) + if (toPolyℝ p).IsRoot (Dyadic.toReal hi) then 1 else 0

Node count. For positive-degree square-free p and lo < hi, the exact Sturm count on (lo, hi] splits as the number of positive roots of the Möbius transform (= the p-roots in the open interval (a, b)) plus the endpoint indicator [p(hi) = 0]. No width budget is needed: the count is exact.

theorem HexRealRootsMathlib.bisect_refute_sector {p : Hex.ZPoly} (hdeg : 1 ≤ Hex.DensePoly.natDegree p) (hp : p.SquareFreeRat) {lo hi : Dyadic} (hlt : lo < hi) (hw : Dyadic.toReal hi - Dyadic.toReal lo ≤ 2 ^ (-↑(Hex.sepPrec p))) (hV2 : 2 ≤ Hex.descartesVar (Hex.mobiusTransform p { lower := lo, upper := hi, lt := hlt })) : False

The V ≥ 2 row is impossible at the depth budget. Two or more transform-roots outside the sector correspond to two distinct roots of p inside the two-circle region, which are closer than 4·2^{−sepPrec p}, contradicting the Mahler separation bound.

theorem HexRealRootsMathlib.bisect_refute_double {p : Hex.ZPoly} (hdeg : 1 ≤ Hex.DensePoly.natDegree p) (hp : p.SquareFreeRat) {lo hi : Dyadic} (hlt : lo < hi) (hw : Dyadic.toReal hi - Dyadic.toReal lo ≤ 2 ^ (-↑(Hex.sepPrec p))) (hV1 : Hex.descartesVar (Hex.mobiusTransform p { lower := lo, upper := hi, lt := hlt }) = 1) (hbz : (Hex.dyadicSign (p.evalDyadic hi) == 0) = true) : False

The V = 1 ∧ p(hi) = 0 row is impossible at the depth budget. It puts two real roots — an interior root and hi — in (lo, hi], a Sturm count of 2, contradicting sturmCount_le_one.

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

The Descartes engine succeeds on nonzero square-free input. For nonzero p passing the executable SquareFreeRat test, ZPoly.isolateDescartes? p ≠ none, so the runtime never falls back to the Sturm engine.

Positive degree is the real content (isolateDescartes?_isSome_of_degree_pos, the two-circle termination argument); a nonzero constant certifies through the empty chain. As with isolateSturm?_isSome, the p ≠ 0 hypothesis is added because SquareFreeRat 0 is vacuous while ZPoly.isolateDescartes? 0 = none.