13.2. Mathlib-free execution🔗

The computational package exposes Hex.ZPoly.isolateRealRoots?, which tries Descartes search before falling back to Sturm bisection. The Hex.ZPoly.isolateDescartes? and Hex.ZPoly.isolateSturm? variants select one engine explicitly; Hex.ZPoly.rootCount and Hex.ZPoly.sturmCount expose the exact counting operations. These functions run in native Lean and need no external oracle at runtime.

The core isolators reject the zero polynomial; positive-degree inputs must be squarefree, while nonzero constants have no roots and return an empty isolation. Every emitted interval carries executable evidence for its Sturm count, ordering, and contribution to the certified total. The core package checks that finite evidence, while HexRealRootsMathlib supplies the theorem connecting it to roots of Polynomial ℝ and handles squarefree reduction for the elaborator below.