16.7. The Mathlib correspondence🔗

Everything the driver computes is executable and Mathlib-free. HexRootsTheory is the companion that interprets it: a Hex.ZPoly input becomes a complex polynomial through HexRootsTheory.toPolyℂ, and the executable certificates become statements about its root set in Polynomial ℂ. The correspondence has two halves. Soundness is HexRootsTheory.isolateComplexRoots?_sound from the certificate section: a successful run enumerates exactly the distinct complex roots, at the requested precision. Completeness is the converse guarantee, that on a nonzero polynomial with only simple roots the search cannot fail, for every strategy and every requested precision:

HexRootsTheory.isolateComplexRoots?_isSome (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy) :
  (p.isolateComplexRoots? h atomPrec strategy).isSome = true
HexRootsTheory.isolateComplexRoots?_isSome
  (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p)
  (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy) :
  (p.isolateComplexRoots? h atomPrec
        strategy).isSome =
    true

Completeness is what lets the total wrapper HexRootsTheory.isolateComplexRoots from the entry-point section drop the Option and return the atom array directly, with its run equation, root count, root set, and precision exposed by the isolate_* theorems shown there. One further guarantee is stated on the wrapper: distinct atoms have disjoint closed circumscribed discs, so the certified enclosures never overlap and each root is separated from every other by exact dyadic data.

HexRootsTheory.isolateComplexRoots_disjoint (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet)
  {i j : ℕ}
  (hi :
    i <
      (HexRootsTheory.isolateComplexRoots p h hp atomPrec
          strategy).size)
  (hj :
    j <
      (HexRootsTheory.isolateComplexRoots p h hp atomPrec
          strategy).size)
  (hij : i ≠ j) :
  Disjoint
    (HexRootsTheory.DyadicSquare.closedDisc
      (HexRootsTheory.isolateComplexRoots p h hp atomPrec
            strategy)[i].square)
    (HexRootsTheory.DyadicSquare.closedDisc
      (HexRootsTheory.isolateComplexRoots p h hp atomPrec
            strategy)[j].square)
HexRootsTheory.isolateComplexRoots_disjoint
  (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p)
  (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy :=
    Hex.AtomStrategy.nkThenPellet)
  {i j : ℕ}
  (hi :
    i <
      (HexRootsTheory.isolateComplexRoots
          p h hp atomPrec strategy).size)
  (hj :
    j <
      (HexRootsTheory.isolateComplexRoots
          p h hp atomPrec strategy).size)
  (hij : i ≠ j) :
  Disjoint
    (HexRootsTheory.DyadicSquare.closedDisc
      (HexRootsTheory.isolateComplexRoots
            p h hp atomPrec
            strategy)[i].square)
    (HexRootsTheory.DyadicSquare.closedDisc
      (HexRootsTheory.isolateComplexRoots
            p h hp atomPrec
            strategy)[j].square)

Behind these statements the companion develops the analysis the certificates rely on: a ported Newton-Kantorovich contraction theorem, the argument principle and Rouché's theorem for counting roots in discs, and the Mahler separation bound that keeps subdivision terminating. None of that analysis runs; it justifies, once and for all, the fixed dyadic comparisons the kernel re-checks.