10.7. Cross-references🔗

HexRealRoots sits at the top of the polynomial stack and is consumed through its Mathlib bridge:

• HexPolyZ provides the dense integer polynomial Hex.ZPoly that the isolator operates on, together with the content, primitive-part, and squarefree-decomposition operations the squarefree-core step relies on.

• HexRealRootsMathlib is the correspondence library. It identifies the executable Sturm certificate with the root theory of Polynomial ℝ, proves that the squarefree core shares the real roots of the original polynomial, and provides Hex.IsolatedRealRoots and the isolate_roots elaborator documented here. The Mathlib dependency lives entirely in this bridge; a Hex.ZPoly input keeps every emitted statement Mathlib-facing only through HexPolyZMathlib.toPolynomial.