9.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; nothing counts until an exact witness rechecks it.

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.isolate entry point below handles.