10.1. Introduction🔗

HexRealRoots isolates the real roots of a polynomial with integer coefficients: it returns disjoint rational intervals, one per real root, each certified to contain exactly one. The isolation is exact. There are no floats and no error budget anywhere in the computation; the endpoints are dyadic rationals and the certificate is a Sturm sign-variation count checked in the kernel.

The computational core is Mathlib-free. It builds the Sturm chain of a polynomial by exact integer arithmetic, evaluates sign variations at dyadic points, and bisects until each root is alone in its interval. The correspondence library HexRealRootsMathlib is the Mathlib bridge: it proves that the isolated intervals really do capture the roots of the polynomial as an element of Polynomial ℝ, and it packages the whole workflow behind a single term elaborator.

The user-facing entry point is isolate_roots. One call inspects a polynomial, runs the exact isolator while the file elaborates, and produces a term whose type records the certified statements. No knowledge of Sturm chains, dyadic arithmetic, or squarefreeness is needed at the call site.