def HexRootsMathlib.Worklist.squares (work : Array Hex.Component) : Array Hex.DyadicSquare

All squares stored by a component worklist.

Equations

• HexRootsMathlib.Worklist.squares work = Array.flatMap (fun (x : Hex.Component) => x.squares) work

def HexRootsMathlib.Worklist.AtPrec (work : Array Hex.Component) (prec : ℤ) : Prop

Every worklist square has the same leaf precision.

Equations

• HexRootsMathlib.Worklist.AtPrec work prec = ∀ c ∈ work.toList, ∀ s ∈ c.squares.toList, s.prec = prec

def HexRootsMathlib.Worklist.Covers (p : Hex.ZPoly) (work : Array Hex.Component) : Prop

Every polynomial root lies in a worklist square.

Equations

• HexRootsMathlib.Worklist.Covers p work = HexRootsMathlib.CoversRoots p (HexRootsMathlib.Worklist.squares work)

theorem HexRootsMathlib.refineAll_mem_prec {p : Hex.ZPoly} {work : Array Hex.Component} {prec : ℤ} (hprec : Worklist.AtPrec work prec) {c : Hex.Component} (hc : c ∈ (Hex.Component.refineAll p work).toList) {s : Hex.DyadicSquare} (hs : s ∈ c.squares.toList) : s.prec = prec + 1

A member of a globally normalized round is one level finer than every input square.

theorem HexRootsMathlib.refineAll_covers {p : Hex.ZPoly} {work : Array Hex.Component} (hcover : Worklist.Covers p work) : Worklist.Covers p (Hex.Component.refineAll p work)

Global subdivision preserves coverage of every complex root.

theorem HexRootsMathlib.refineAll_nodup (p : Hex.ZPoly) (work : Array Hex.Component) : (Hex.Component.refineAll p work).toList.Nodup

A normalized round never duplicates an outer component.

theorem HexRootsMathlib.refineAll_roots_ne {p : Hex.ZPoly} {work : Array Hex.Component} {prec : ℤ} (hprec : Worklist.AtPrec work prec) {c d : Hex.Component} (hc : c ∈ (Hex.Component.refineAll p work).toList) (hd : d ∈ (Hex.Component.refineAll p work).toList) (hcd : c ≠ d) {z w : ℂ} (hzc : z ∈ Component.region c) (hwd : w ∈ Component.region d) : z ≠ w

Distinct normalized components cannot designate the same root: squares containing that root would be adjacent and hence glued together.

theorem HexRootsMathlib.refineAll_component_root {p : Hex.ZPoly} {work : Array Hex.Component} {prec : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) ≤ prec + 1) (hprec : Worklist.AtPrec work prec) (hcover : Worklist.Covers p work) {c : Hex.Component} (hc : c ∈ (Hex.Component.refineAll p work).toList) : ∃ (z : ℂ), (toPolyℂ p).IsRoot z ∧ z ∈ Component.region c

Every output component of a globally normalized separation-depth round actually contains one polynomial root.

theorem HexRootsMathlib.witness_quadrupled_of_glueCovered {p : Hex.ZPoly} {squares component : Array Hex.DyadicSquare} {prec : ℤ} {z : ℂ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec) (hprec : ∀ u ∈ squares.toList, u.prec = prec) (hkeep : ∀ u ∈ squares.toList, Hex.rootFree p u ≠ true) (hc : component ∈ (Hex.glueCovered squares).toList) (hzroot : (toPolyℂ p).IsRoot z) (hzcomponent : z ∈ Component.region { squares := component, candidateK := 1 }) : Hex.TaylorShift.witnessCheck (Hex.encSquare component).doubled.doubled (Hex.TaylorShift.compute p (Hex.encSquare component).doubled.doubled.center) 1 = true

A root-bearing maximal survivor component has enough uniform recentring margin on its quadrupled enclosing square for the exact Taylor Pellet witness. Five leaf levels pay for the enclosing-square loss and quadrupling while the implemented separation slack controls the remote-root tail.

theorem HexRootsMathlib.certify_pellet_of_glueCovered {p : Hex.ZPoly} {squares component : Array Hex.DyadicSquare} {prec target : ℤ} {z : ℂ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec) (htarget : target + 5 ≤ prec) (hprec : ∀ u ∈ squares.toList, u.prec = prec) (hkeep : ∀ u ∈ squares.toList, Hex.rootFree p u ≠ true) (hc : component ∈ (Hex.glueCovered squares).toList) (hzroot : (toPolyℂ p).IsRoot z) (hzcomponent : z ∈ Component.region { squares := component, candidateK := 1 }) : ∃ (iso : Hex.DyadicRootIsolation p), Hex.Component.certify? p Hex.AtomStrategy.pellet { squares := component, candidateK := 1 } = some (Hex.Certified.atom iso) ∧ target ≤ iso.square.prec ∧ z ∈ Certified.region (Hex.Certified.atom iso)

At the globally normalized completeness depth, the Pellet-only strategy's first candidate is the root-bearing k = 1 witness. It therefore returns a target-ready atom, whether or not the guarded speculative step is adopted.

theorem HexRootsMathlib.certify_atom_of_glueCovered {p : Hex.ZPoly} {squares component : Array Hex.DyadicSquare} {prec target : ℤ} {z : ℂ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec) (htarget : target + 5 ≤ prec) (hprec : ∀ u ∈ squares.toList, u.prec = prec) (hkeep : ∀ u ∈ squares.toList, Hex.rootFree p u ≠ true) (hc : component ∈ (Hex.glueCovered squares).toList) (hzroot : (toPolyℂ p).IsRoot z) (hzcomponent : z ∈ Component.region { squares := component, candidateK := 1 }) (strategy : Hex.AtomStrategy) : ∃ (iso : Hex.DyadicRootIsolation p), Hex.Component.certify? p strategy { squares := component, candidateK := 1 } = some (Hex.Certified.atom iso) ∧ target ≤ iso.square.prec ∧ z ∈ Certified.region (Hex.Certified.atom iso)

Every root-bearing maximal component at the normalized depth certifies as a target-ready atom for each of the three executable atom strategies.

theorem HexRootsMathlib.refineAll_component_certifies {p : Hex.ZPoly} {work : Array Hex.Component} {prec target : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec + 1) (htarget : target + 5 ≤ prec + 1) (hprec : Worklist.AtPrec work prec) (hcover : Worklist.Covers p work) (strategy : Hex.AtomStrategy) {c : Hex.Component} (hc : c ∈ (Hex.Component.refineAll p work).toList) : ∃ (z : ℂ) (iso : Hex.DyadicRootIsolation p), (toPolyℂ p).IsRoot z ∧ z ∈ Component.region c ∧ Hex.Component.certify? p strategy c = some (Hex.Certified.atom iso) ∧ target ≤ iso.square.prec ∧ z ∈ Certified.region (Hex.Certified.atom iso)

Every component produced by the last normalized round has a designated root and succeeds as a target-ready atom under the selected strategy.

theorem HexRootsMathlib.refineAll_certificates_disjoint {p : Hex.ZPoly} {work : Array Hex.Component} {prec target : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec + 1) (htarget : target + 5 ≤ prec + 1) (hsepTarget : ↑(Hex.separationDepth p) ≤ target) (hprec : Worklist.AtPrec work prec) (hcover : Worklist.Covers p work) (strategy : Hex.AtomStrategy) {c d : Hex.Component} (hc : c ∈ (Hex.Component.refineAll p work).toList) (hd : d ∈ (Hex.Component.refineAll p work).toList) (hcd : c ≠ d) {r q : Hex.Certified p} (hr : Hex.Component.certify? p strategy c = some r) (hq : Hex.Component.certify? p strategy d = some q) : r.square.discsMeet q.square = false

Certificates of two distinct final normalized components have a negative executable disc-intersection test.

theorem HexRootsMathlib.refineAll_normalized {p : Hex.ZPoly} {work : Array Hex.Component} {prec target : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec + 1) (htarget : target + 5 ≤ prec + 1) (hnormal : Hex.completenessDepth p target ≤ prec + 1) (hprec : Worklist.AtPrec work prec) (hcover : Worklist.Covers p work) (strategy : Hex.AtomStrategy) : Hex.IsolationLoop.normalized p target (Hex.IsolationLoop.attempts p strategy (Hex.Component.refineAll p work)) = true

The last normalized round has reached the executable depth guard.

theorem HexRootsMathlib.refineAll_allReady {p : Hex.ZPoly} {work : Array Hex.Component} {prec target : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec + 1) (htarget : target + 5 ≤ prec + 1) (hprec : Worklist.AtPrec work prec) (hcover : Worklist.Covers p work) (strategy : Hex.AtomStrategy) : Hex.IsolationLoop.allReady target (Hex.IsolationLoop.attempts p strategy (Hex.Component.refineAll p work)) = true

Every attempt on the final normalized worklist succeeds at target precision.

theorem HexRootsMathlib.refineAll_disjoint {p : Hex.ZPoly} {work : Array Hex.Component} {prec target : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec + 1) (htarget : target + 5 ≤ prec + 1) (hsepTarget : ↑(Hex.separationDepth p) ≤ target) (hprec : Worklist.AtPrec work prec) (hcover : Worklist.Covers p work) (strategy : Hex.AtomStrategy) : Hex.IsolationLoop.disjoint (Hex.IsolationLoop.attempts p strategy (Hex.Component.refineAll p work)) = true

Successful attempts on the final normalized worklist pass the exact pairwise disc-disjointness check.

theorem HexRootsMathlib.refineAll_outputs_atoms {p : Hex.ZPoly} {work : Array Hex.Component} {prec target : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec + 1) (htarget : target + 5 ≤ prec + 1) (hprec : Worklist.AtPrec work prec) (hcover : Worklist.Covers p work) (strategy : Hex.AtomStrategy) (r : Hex.Certified p) : r ∈ (Hex.IsolationLoop.outputs (Hex.IsolationLoop.attempts p strategy (Hex.Component.refineAll p work))).toList → ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso

Every successful attempt in the final normalized round is an atom.

theorem HexRootsMathlib.isolateLoop_refineAll_success {p : Hex.ZPoly} {work : Array Hex.Component} {prec target : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hdepth : ↑(Hex.separationDepth p) + 5 ≤ prec + 1) (htarget : target + 5 ≤ prec + 1) (hsepTarget : ↑(Hex.separationDepth p) ≤ target) (hnormal : Hex.completenessDepth p target ≤ prec + 1) (hprec : Worklist.AtPrec work prec) (hcover : Worklist.Covers p work) (strategy : Hex.AtomStrategy) (fuel : ℕ) : ∃ (rs : Array (Hex.Certified p)), Hex.isolateLoop p target strategy (fuel + 1) (Hex.Component.refineAll p work) = some rs ∧ ∀ r ∈ rs.toList, ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso

Once the last global round has been formed, one positive fuel step emits its target-ready, pairwise-disjoint atom certificates.

theorem HexRootsMathlib.isolateLoop_complete_of_fuel {p : Hex.ZPoly} {target prec : ℤ} {strategy : Hex.AtomStrategy} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hsepTarget : ↑(Hex.separationDepth p) ≤ target) {work : Array Hex.Component} (hprec : Worklist.AtPrec work prec) (hcover : Worklist.Covers p work) (hlt : prec < Hex.completenessDepth p target) {fuel : ℕ} (hfuel : (Hex.completenessDepth p target - prec).toNat < fuel) : ∃ (rs : Array (Hex.Certified p)), Hex.isolateLoop p target strategy fuel work = some rs ∧ ∀ r ∈ rs.toList, ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso

Sufficient fuel carries any globally normalized worklist to the fixed completeness depth and then emits atoms.

theorem HexRootsMathlib.isolateAll_cauchy_complete {p : Hex.ZPoly} {target : ℤ} (hp : toPolyℂ p ≠ 0) (hsize : 1 < Hex.DensePoly.size p) (hsep : (HexPolyZMathlib.toPolyℚ p).Separable) (hsepTarget : ↑(Hex.separationDepth p) ≤ target) (strategy : Hex.AtomStrategy) (hd : 0 < Hex.DensePoly.natDegree p) : ∃ (rs : Array (Hex.Certified p)), Hex.isolateAll? p target #[Hex.Component.cauchy p hd] strategy = some rs ∧ ∀ r ∈ rs.toList, ∃ (iso : Hex.DyadicRootIsolation p), r = Hex.Certified.atom iso

The executable fuelFor budget is sufficient for a Cauchy-started run, for every atom strategy.

theorem HexRootsMathlib.isolateComplexRoots?_exists (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ) (strategy : Hex.AtomStrategy) : ∃ (atoms : Array (Hex.DyadicRootIsolation p)), p.isolateComplexRoots? h atomPrec strategy = some atoms

Every nonzero squarefree executable polynomial is successfully isolated by each atom strategy. Nonzero constants take the explicit empty-output branch; positive-degree inputs use the complete Cauchy-started driver.

theorem HexRootsMathlib.isolateComplexRoots?_spec (p : Hex.ZPoly) (h : Hex.HasOnlySimpleRoots p) (hp : p ≠ 0) (atomPrec : ℤ) (strategy : Hex.AtomStrategy := Hex.AtomStrategy.nkThenPellet) : ∃ (atoms : Array (Hex.DyadicRootIsolation p)), p.isolateComplexRoots? h atomPrec strategy = some atoms ∧ atoms.size = (toPolyℂ p).natDegree ∧ (List.map DyadicRootIsolation.root atoms.toList).toFinset = (toPolyℂ p).roots.toFinset ∧ ∀ iso ∈ atoms.toList, atomPrec ≤ iso.square.prec

A nonzero squarefree polynomial has a successful isolation whose atoms enumerate its complex roots exactly, without duplicates, at the requested precision. This bundles driver completeness with the principal soundness contracts for proof-facing clients.

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

Boolean isSome form of full driver completeness.