12.2. The ZPoly.isolateComplexRoots? entry point🔗

For a nonzero polynomial with only simple roots, Hex.ZPoly.isolateComplexRoots? runs the whole isolator and returns some array of atoms, one per distinct complex root. It is Option-valued for the degenerate inputs the precondition still admits: the zero polynomial, which has every point as a root, gives none, and a nonzero constant gives some #[]. It takes the polynomial as a Hex.ZPoly (the Mathlib-free dense integer polynomial), a proof that the roots are simple, a target precision in bits, and a choice of which atom certificate to attempt:

Hex.ZPoly.isolateComplexRoots? (p : Hex.ZPoly)
  (_h : Hex.HasOnlySimpleRoots p) (atom_prec : ℤ)
  (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) :
  Option (Array (Hex.DyadicRootIsolation p))
Hex.ZPoly.isolateComplexRoots?
  (p : Hex.ZPoly)
  (_h : Hex.HasOnlySimpleRoots p)
  (atom_prec : ℤ)
  (strategy : Hex.AtomStrategy :=
    Hex.AtomStrategy.nkThenPellet) :
  Option
    (Array (Hex.DyadicRootIsolation p))

The simple-root precondition is decidable, so discharging it is a matter of by decide in the common case, or a companion lemma for a named polynomial. It casts the polynomial and its derivative to rationals and checks that their gcd is constant:

Hex.HasOnlySimpleRoots (p : Hex.ZPoly) : Prop
Hex.HasOnlySimpleRoots (p : Hex.ZPoly) :
  Prop

Proof-facing clients can avoid Option entirely. The companion's total wrapper requires the missing nonzero hypothesis and uses the driver completeness theorem to return the array directly:

HexRootsMathlib.isolateComplexRoots (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) :
  Array (Hex.DyadicRootIsolation p)
HexRootsMathlib.isolateComplexRoots
  (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p)
  (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy :=
    Hex.AtomStrategy.nkThenPellet) :
  Array (Hex.DyadicRootIsolation p)

Completeness selects the wrapper's value from a successful executable run, and its principal theorems expose that run equation, the exact root count, the complete root set, and the requested precision:

HexRootsMathlib.isolateComplexRoots_eq (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) :
  p.isolateComplexRoots? h atomPrec strategy =
    some (HexRootsMathlib.isolateComplexRoots p h hp atomPrec strategy)
HexRootsMathlib.isolateComplexRoots_eq
  (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p)
  (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy :=
    Hex.AtomStrategy.nkThenPellet) :
  p.isolateComplexRoots? h atomPrec
      strategy =
    some
      (HexRootsMathlib.isolateComplexRoots
        p h hp atomPrec strategy)

HexRootsMathlib.isolateComplexRoots_count (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) :
  (HexRootsMathlib.isolateComplexRoots p h hp atomPrec strategy).size =
    (HexRootsMathlib.toPolyℂ p).natDegree
HexRootsMathlib.isolateComplexRoots_count
  (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p)
  (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy :=
    Hex.AtomStrategy.nkThenPellet) :
  (HexRootsMathlib.isolateComplexRoots p h
        hp atomPrec strategy).size =
    (HexRootsMathlib.toPolyℂ p).natDegree

HexRootsMathlib.isolateComplexRoots_roots (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) :
  (List.map HexRootsMathlib.DyadicRootIsolation.root
        (HexRootsMathlib.isolateComplexRoots p h hp atomPrec
            strategy).toList).toFinset =
    (HexRootsMathlib.toPolyℂ p).roots.toFinset
HexRootsMathlib.isolateComplexRoots_roots
  (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p)
  (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy :=
    Hex.AtomStrategy.nkThenPellet) :
  (List.map
        HexRootsMathlib.DyadicRootIsolation.root
        (HexRootsMathlib.isolateComplexRoots
            p h hp atomPrec
            strategy).toList).toFinset =
    (HexRootsMathlib.toPolyℂ
          p).roots.toFinset

HexRootsMathlib.isolateComplexRoots_prec (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet)
  (iso : Hex.DyadicRootIsolation p) :
  iso ∈
      (HexRootsMathlib.isolateComplexRoots p h hp atomPrec
          strategy).toList →
    atomPrec ≤ iso.square.prec
HexRootsMathlib.isolateComplexRoots_prec
  (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p)
  (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy :=
    Hex.AtomStrategy.nkThenPellet)
  (iso : Hex.DyadicRootIsolation p) :
  iso ∈
      (HexRootsMathlib.isolateComplexRoots
          p h hp atomPrec
          strategy).toList →
    atomPrec ≤ iso.square.prec

The strategy argument, a Hex.AtomStrategy, selects which certificate form the driver attempts, and in which order: .nk for the Newton-Kantorovich witness alone, .pellet for the Pellet witness alone, and .nkThenPellet (the general default) for the former with the latter as fallback. The two tests differ in what they need: the Newton-Kantorovich witness certifies on the doubled square and gives the sharper enclosure, but it needs the derivative to dominate there, which fails near a cluster of roots; the Pellet witness certifies on the quadrupled square by a coefficient inequality, so it still succeeds in that case. Trying Newton first and falling back to Pellet therefore certifies more squares than either alone, and avoids subdividing further just to satisfy Newton. The explicit single-form strategies let either certificate be selected or benchmarked on its own; callers with no such need pick the default.

The precision is an integer lower bound on each returned square's prec, so its half-width is at most 2⁻ᵖʳᵉᶜ. The driver also floors this target at the polynomial's separation precision; asking for a coarser or even negative precision never makes distinct roots overlap, and the returned squares may be finer than requested. For a nonzero simple-root polynomial every strategy succeeds by the companion completeness theorem. Multiple roots do not satisfy the precondition: callers that need them use Hex.isolateAll?, whose successful output may contain Pellet clusters and whose none records failure to reach the certified emission condition within its structural fuel.

Each returned atom is one square with its certificate. The certified region depends on which disjunct fired, so consumers rely only on the shared consequence: exactly one root lies in the certified region, and that region sits inside the stored square's circumscribed disc.

Hex.DyadicRootIsolation (p : Hex.ZPoly) : Type
Hex.DyadicRootIsolation (p : Hex.ZPoly) :
  Type

Hex.DyadicRootIsolation.mk

square : Hex.DyadicSquare

witness : Hex.AtomCertificate p self.square