12.4. What the certificate proves🔗

A successful Hex.ZPoly.isolateComplexRoots? run is not just a list of squares; the companion reads a complete root enumeration out of it. Each atom names a genuine complex root, distinct atoms name distinct roots, and together they exhaust the root set:

theorem

HexRootsMathlib.isolateComplexRoots?_sound (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy)
  {atoms : Array (Hex.DyadicRootIsolation p)}
  (hrun : p.isolateComplexRoots? h atomPrec strategy = some atoms) :
  (List.map HexRootsMathlib.DyadicRootIsolation.root
          atoms.toList).toFinset =
      (HexRootsMathlib.toPolyℂ p).roots.toFinset ∧
    ∀ iso ∈ atoms.toList, atomPrec ≤ iso.square.prec
HexRootsMathlib.isolateComplexRoots?_sound
  (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p)
  (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy)
  {atoms :
    Array (Hex.DyadicRootIsolation p)}
  (hrun :
    p.isolateComplexRoots? h atomPrec
        strategy =
      some atoms) :
  (List.map
          HexRootsMathlib.DyadicRootIsolation.root
          atoms.toList).toFinset =
      (HexRootsMathlib.toPolyℂ
            p).roots.toFinset ∧
    ∀ iso ∈ atoms.toList,
      atomPrec ≤ iso.square.prec

Successful isolation enumerates exactly the distinct complex roots and meets the requested precision, for every strategy and every executable edge case.

The root an atom names is a semantic value, not part of the executable data. The companion selects it from the atom's certificate:

def

HexRootsMathlib.DyadicRootIsolation.root {p : Hex.ZPoly}
  (iso : Hex.DyadicRootIsolation p) : ℂ
HexRootsMathlib.DyadicRootIsolation.root
  {p : Hex.ZPoly}
  (iso : Hex.DyadicRootIsolation p) : ℂ

The unique complex root selected by an atom certificate.

Because the semantic roots of the returned atoms are exactly (toPolyℂ p).roots.toFinset, listing the atoms is a complete case analysis of the complex roots, the same way real-root isolation gives a complete analysis of the real roots. The Pisot example above is one instance: its three atoms account for every root, so bounding each atom bounds every root.