12.1. Introduction🔗

HexRoots isolates the complex roots of a polynomial with integer coefficients. Each root is enclosed in a square in the complex plane with Gaussian-dyadic centre and power-of-two half-width, carrying a witness, checked by decide, that a certified region around the square holds exactly one root. As with real-root isolation the certificates are exact: the Taylor coefficients at the centre are exact Gaussian dyadics, and every witness is a strict comparison between two dyadic rationals, with no floats and no error budget. The search may use approximate dyadic reciprocals to place candidate squares, but those are only hints.

The computational core is Mathlib-free. It expands a polynomial about a Gaussian-dyadic centre, tests candidate squares, subdivides, and glues the survivors into connected components until each root sits alone in a certified region. The correspondence library HexRootsMathlib is the Mathlib companion: it proves that a certificate really does pin down a root of the polynomial viewed as an element of Polynomial ℂ, and that a successful whole-polynomial run enumerates every distinct root exactly once.

A single root is an atom. Atoms admit two interchangeable certificate forms: a Newton-Kantorovich contraction witness, whose certified region is the square itself, and a Pellet root-count witness, whose certified region is the square's circumscribed disc. A component that a Pellet witness certifies to hold k ≥ 2 roots with multiplicity, most naturally a repeated root, is reported instead as a cluster. A nonzero polynomial with only simple roots isolates entirely into atoms; that is the case the user-facing Hex.ZPoly.isolateComplexRoots? entry point below handles.