theorem HexRootsMathlib.isolateLoop_nk_atoms {p : Hex.ZPoly} {target : ℤ} {fuel : ℕ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hloop : Hex.isolateLoop p target Hex.AtomStrategy.nk fuel work = some rs) (r : Hex.Certified p) : r ∈ rs.toList → ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso ∧ Hex.nkWitness p iso.square ∧ iso.witness.isNK = true

Every successful NK-only loop result is an NK atom.

theorem HexRootsMathlib.isolateAll_nk_covers {p : Hex.ZPoly} {target : ℤ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target work Hex.AtomStrategy.nk = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) (hz : z ∈ Worklist.region work) : z ∈ Results.region rs

Successful NK-only isolateAll? execution preserves every root covered by its starting worklist.

theorem HexRootsMathlib.isolateAll_nk_atoms {p : Hex.ZPoly} {target : ℤ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target work Hex.AtomStrategy.nk = some rs) (r : Hex.Certified p) : r ∈ rs.toList → ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso ∧ Hex.nkWitness p iso.square ∧ iso.witness.isNK = true

Every successful NK-only isolateAll? result is an NK atom.

theorem HexRootsMathlib.isolateAll_nk_ready_disjoint {p : Hex.ZPoly} {target : ℤ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target work Hex.AtomStrategy.nk = some rs) : (∀ r ∈ rs.toList, target ≤ r.square.prec) ∧ ∀ {i j : ℕ} (hi : i < rs.size) (hj : j < rs.size), i ≠ j → Disjoint (DyadicSquare.closedDisc rs[i].square) (DyadicSquare.closedDisc rs[j].square)

Successful NK-only isolateAll? results meet the target and have pairwise-disjoint closed circumscribed discs.

theorem HexRootsMathlib.isolateAll_nk_cauchy_covers (p : Hex.ZPoly) (hdegree : 0 < Hex.DensePoly.natDegree p) {target : ℤ} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target #[Hex.Component.cauchy p hdegree] Hex.AtomStrategy.nk = some rs) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) : z ∈ Results.region rs

Starting from the Cauchy component, successful NK-only isolation covers every complex root.

theorem HexRootsMathlib.isolateAll_nk_simple {p : Hex.ZPoly} {target : ℤ} {work : Array Hex.Component} {rs : Array (Hex.Certified p)} (hrun : Hex.isolateAll? p target work Hex.AtomStrategy.nk = some rs) {i : ℕ} (hi : i < rs.size) : ∃ (iso : Hex.DyadicRootIsolation p), rs[i] = Hex.Certified.atom iso ∧ ∃ (z : ℂ), Polynomial.eval z (toPolyℂ p) = 0 ∧ z ∈ DyadicSquare.openSquare iso.square ∧ Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0 ∧ ∀ (w : ℂ), Polynomial.eval w (toPolyℂ p) = 0 → w ∈ DyadicSquare.closedSquare iso.square → w = z

Each emitted NK atom contains one interior simple root, unique in its closed square.

theorem HexRootsMathlib.isolate_nk_run (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (hdegree : 0 < Hex.DensePoly.natDegree p) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec Hex.AtomStrategy.nk = some atoms) : ∃ (rs : Array (Hex.Certified p)), Hex.isolateAll? p (max atomPrec ↑(Hex.separationDepth p)) #[Hex.Component.cauchy p hdegree] Hex.AtomStrategy.nk = some rs ∧ rs.size = atoms.size ∧ ∀ (i : ℕ) (hi : i < rs.size) (hj : i < atoms.size), rs[i] = Hex.Certified.atom atoms[i] ∧ Hex.nkWitness p atoms[i].square ∧ atoms[i].witness.isNK = true

In the positive-degree branch, successful ZPoly.isolateComplexRoots? execution is a successful Cauchy-started isolateAll? run whose result indices correspond exactly to the returned NK atoms.

theorem HexRootsMathlib.isolate_nk_simple (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (hdegree : 0 < Hex.DensePoly.natDegree p) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec Hex.AtomStrategy.nk = some atoms) {i : ℕ} (hi : i < atoms.size) : atomPrec ≤ atoms[i].square.prec ∧ Hex.nkWitness p atoms[i].square ∧ ∃ (z : ℂ), Polynomial.eval z (toPolyℂ p) = 0 ∧ z ∈ DyadicSquare.openSquare atoms[i].square ∧ Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0 ∧ ∀ (w : ℂ), Polynomial.eval w (toPolyℂ p) = 0 → w ∈ DyadicSquare.closedSquare atoms[i].square → w = z

Every atom returned by positive-degree NK-only isolation meets the requested precision and contains a unique interior simple root.

theorem HexRootsMathlib.isolate_nk_disjoint (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (hdegree : 0 < Hex.DensePoly.natDegree p) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec Hex.AtomStrategy.nk = some atoms) {i j : ℕ} (hi : i < atoms.size) (hj : j < atoms.size) (hij : i ≠ j) : Disjoint (DyadicSquare.closedDisc atoms[i].square) (DyadicSquare.closedDisc atoms[j].square)

Distinct atoms returned by positive-degree NK-only isolation have disjoint closed circumscribed discs.

theorem HexRootsMathlib.isolate_nk_covers_once_of_pos (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (hdegree : 0 < Hex.DensePoly.natDegree p) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec Hex.AtomStrategy.nk = some atoms) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) : ∃! i : Fin atoms.size, z ∈ DyadicSquare.closedSquare atoms[i].square

Every complex root belongs to exactly one atom returned by successful positive-degree NK-only isolation.

theorem HexRootsMathlib.toPolyℂ_ne_zero (p : Hex.ZPoly) (hp : Hex.DensePoly.size p ≠ 0) : toPolyℂ p ≠ 0

A nonzero executable polynomial has a nonzero complex cast.

theorem HexRootsMathlib.not_isRoot_of_degree_not_pos (p : Hex.ZPoly) (hp : Hex.DensePoly.size p ≠ 0) (hdegree : ¬0 < Hex.DensePoly.natDegree p) (z : ℂ) : ¬(toPolyℂ p).IsRoot z

A nonzero executable polynomial whose natural degree is not positive has no complex root.

theorem HexRootsMathlib.isolate_nk_nonpositive (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) (hdegree : ¬0 < Hex.DensePoly.natDegree p) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec Hex.AtomStrategy.nk = some atoms) : Hex.DensePoly.size p ≠ 0 ∧ atoms = #[]

A successful non-positive-degree ZPoly.isolateComplexRoots? call is exactly the nonzero constant branch and returns the empty atom array.

theorem HexRootsMathlib.isolate_nk_covers_once (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec Hex.AtomStrategy.nk = some atoms) {z : ℂ} (hzroot : (toPolyℂ p).IsRoot z) : ∃! i : Fin atoms.size, z ∈ DyadicSquare.closedSquare atoms[i].square

Every successful NK-only ZPoly.isolateComplexRoots? call assigns each complex root to exactly one returned atom, including the vacuous nonzero-constant branch.

theorem HexRootsMathlib.isolate_nk_pairwise (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec Hex.AtomStrategy.nk = some atoms) {i j : ℕ} (hi : i < atoms.size) (hj : j < atoms.size) (hij : i ≠ j) : Disjoint (DyadicSquare.closedDisc atoms[i].square) (DyadicSquare.closedDisc atoms[j].square)

Any two differently indexed atoms returned by successful NK-only ZPoly.isolateComplexRoots? execution have disjoint closed circumscribed discs.

theorem HexRootsMathlib.isolate_nk_atom_sound (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (atomPrec : ℤ) {atoms : Array (Hex.DyadicRootIsolation p)} (hrun : p.isolateComplexRoots? h atomPrec Hex.AtomStrategy.nk = some atoms) {i : ℕ} (hi : i < atoms.size) : atomPrec ≤ atoms[i].square.prec ∧ Hex.nkWitness p atoms[i].square ∧ ∃ (z : ℂ), Polynomial.eval z (toPolyℂ p) = 0 ∧ z ∈ DyadicSquare.openSquare atoms[i].square ∧ Polynomial.eval z (Polynomial.derivative (toPolyℂ p)) ≠ 0 ∧ ∀ (w : ℂ), Polynomial.eval w (toPolyℂ p) = 0 → w ∈ DyadicSquare.closedSquare atoms[i].square → w = z

Every returned atom of successful NK-only isolation meets the requested precision and has the unique interior simple-root contract.