def Hex.Certified.asAtom? {p : ZPoly} : Certified p → Option (DyadicRootIsolation p)

Extract an atom from a certified result, failing on clusters.

Equations

• (Hex.Certified.atom iso).asAtom? = some iso
• (Hex.Certified.cluster cl).asAtom? = none

def Hex.isolateAll? (p : ZPoly) (target : Int) (worklist : Array Component) (strategy : AtomStrategy := AtomStrategy.nkThenPellet) : Option (Array (Certified p))

Refine every component to precision at least target and require the circumscribed discs of the certified squares to be pairwise disjoint. Before completenessDepth, refinement is global so rootless survivor halos rejoin the root-bearing component. The fuel is sized from the worklist's coarsest precision so the loop reaches stopDepth p target. none means the full emission condition was not reached within that fuel bound.

Equations

• One or more equations did not get rendered due to their size.

def Hex.ZPoly.isolateComplexRoots? (p : ZPoly) (_h : HasOnlySimpleRoots p) (atom_prec : Int) (strategy : AtomStrategy := AtomStrategy.nkThenPellet) : Option (Array (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.

Equations

• One or more equations did not get rendered due to their size.

def Hex.isolateOne? (p : ZPoly) (atomPrec : Int) (seed : DyadicSquare) (strategy : AtomStrategy := AtomStrategy.nkThenPellet) : Option (RefinedIsolation p)

Start a local search for one simple root from a caller-selected square and refine its atom to at least max atomPrec (mahlerPrec p). This is a deliberately local search: unlike Hex.ZPoly.isolateComplexRoots?, it neither certifies every root nor establishes pairwise disjointness against roots outside the returned atom. The self-contained Hex.AtomCertificate is exactly the weaker fact needed by Hex.SimpleRoot.mk. The returned atom is not promised to lie inside seed; seed selects the initial search region. none means the search was exhausted or the bounded search did not find an atom.

Equations

• One or more equations did not get rendered due to their size.

def Hex.RefinedIsolation.refineTo? {p : ZPoly} (r : RefinedIsolation p) (target : Int) (strategy : AtomStrategy := AtomStrategy.nkThenPellet) : Option { r' : RefinedIsolation p // SimpleRoot.mk r' = SimpleRoot.mk r }

Refine a refined isolation, staying in the refined type and returning the proof that the result isolates the same root. The refinement target is floored at mahlerPrec p so the subtype re-wrap always succeeds on a some, and the identity proof comes from the decidable Intersects re-check via Quot.sound. This is the threading-pattern operation the SimpleRoot module docstring describes: refine once, store the returned representative, and substitute it wherever the original was used.

Equations

• One or more equations did not get rendered due to their size.