9.2. The `isolate` entry point🔗

For a nonzero polynomial with only simple roots, Hex.isolate 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:

def

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

All-atoms output for polynomials with only simple roots: run Hex.isolateAll? from Hex.Component.cauchy with target := max atom_prec (separationDepth p), and require every result to be an atom. none if Hex.isolateAll? fails or (impossible for squarefree p, proven in the companion) some result is a k ≥ 2 cluster. Hex.HasOnlySimpleRoots does not force positive degree, so the degenerate inputs are pinned here: a nonzero constant returns some #[] (no roots to isolate), and the zero polynomial returns none.

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:

def

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

p has only simple complex roots when the executable rational gcd of p and p' is constant. This is definitionally Hex.ZPoly.SquareFreeRat; the Mathlib bridge proves its equivalence to polynomial squarefreeness when p ≠ 0.

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:

def

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

Isolate all complex roots of a nonzero squarefree integer polynomial.

Unlike Hex.isolate, this proof-facing wrapper cannot return none: its required hypotheses discharge the driver's completeness conditions. The result is characterized by isolate!_eq as the successful executable output, with the same atom strategy and requested-precision parameters.

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:

theorem

HexRootsMathlib.isolate!_eq (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) :
  Hex.isolate p h atomPrec strategy =
    some (HexRootsMathlib.isolate! p h hp atomPrec strategy)
HexRootsMathlib.isolate!_eq
  (p : Hex.ZPoly)
  (h : Hex.HasOnlySimpleRoots p)
  (hp : p ≠ 0) (atomPrec : ℤ)
  (strategy : Hex.AtomStrategy :=
    Hex.AtomStrategy.nkThenPellet) :
  Hex.isolate p h atomPrec strategy =
    some
      (HexRootsMathlib.isolate! p h hp
        atomPrec strategy)

The total wrapper is exactly the successful result of Hex.isolate.

theorem

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

The total wrapper returns one atom for each complex root, counted with multiplicity.

theorem

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

The semantic roots selected by the returned atoms are exactly the roots of the input polynomial.

theorem

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

Every returned atom meets the requested precision.

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 explicit single-form strategies let either certificate be selected or benchmarked on its own; callers with no such need pick the default.

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.

structure

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

An atom: one square whose certified region (the square itself for the Newton-Kantorovich disjunct, the circumscribed disc for the Pellet disjunct) contains exactly one simple root.

Constructor

Hex.DyadicRootIsolation.mk

Fields

square : Hex.DyadicSquare

The isolating square.

witness : Hex.AtomCertificate p self.square

An NK/Pellet atom certificate, possibly transported through reflection.

9.2. The isolate entry point🔗

9.2. The `isolate` entry point🔗