9.7. Cross-references🔗

HexRoots sits at the top of the polynomial stack, alongside the real-root isolator, and is consumed through its Mathlib companion:

• HexPolyZ provides the dense integer polynomial Hex.ZPoly the isolator operates on, together with the rational polynomial gcd the simple-root test casts to and reduces.

• HexRealRoots is the real-line analogue. It isolates the real roots with a Sturm sign-variation certificate and returns rational intervals; HexRoots isolates every complex root with dyadic squares. A polynomial's real roots appear in both, as intervals there and, here, among the complex atoms, each lying in its atom's certified region.

• HexRootsMathlib is the correspondence library. It ports the Newton-Kantorovich theorem and develops the argument principle, Rouché's theorem, and the Mahler separation bound for polynomials on circles, then proves soundness and completeness of the isolator: every certificate names the roots it claims, and Hex.isolate never fails on a nonzero squarefree input. The Mathlib dependency lives entirely in this companion; a Hex.ZPoly input keeps the executable core Mathlib-free.