def Hex.stopSlack : Nat

The fixed give-up margin above separationDepth used by stopDepth. Overshooting costs only a few extra subdivision rounds in the rare case certification had not already happened, and nothing else. The globally normalized prefix ends three levels before this bound.

Equations

• Hex.stopSlack = 8

def Hex.stopDepth (p : ZPoly) (target : Int) : Int

The depth at which the drivers give up, max target (separationDepth p) + stopSlack. A none from a driver means that its full emission condition was not reached within this fuel bound.

Equations

• Hex.stopDepth p target = max target ↑(Hex.separationDepth p) + ↑Hex.stopSlack

def Hex.completenessDepth (p : ZPoly) (target : Int) : Int

The depth through which the Cauchy-started driver uses globally glued, uniform subdivision rounds. Two levels pay for encSquare; the other three cover the quadrupled Pellet base (or doubled NK base) with one strict margin level.

Equations

• Hex.completenessDepth p target = max target ↑(Hex.separationDepth p) + 5

def Hex.Component.prec (c : Component) : Int

The common prec of a component's squares (0 for the empty component, which the drivers never produce).

Equations

• c.prec = (Option.map (fun (x : Hex.DyadicSquare) => x.prec) c.squares[0]?).getD 0

def Hex.Certified.square {p : ZPoly} : Certified p → DyadicSquare

The stored square of a certification result: the atom's square, or the cluster's enclosing square. The separation check and the emission precision test read this.

Equations

• (Hex.Certified.atom iso).square = iso.square
• (Hex.Certified.cluster cl).square = Hex.encSquare cl.squares

def Hex.Certified.toComponent {p : ZPoly} : Certified p → Component

Re-enter a certification result into the worklist as a component.

The retained square must cover the certified region, not merely be certified: refinement preserves exactly the roots that lie in the retained squares themselves (children partition the square, and the T₀ discard is sound), while a Pellet certificate counts roots in the stored square's circumscribed disc. A root in the disc but outside the square would be silently lost by the next subdivision; with repeated Newton-jump adoptions this loses far roots of a many-root cluster (the certified disc shrinks toward the cluster's Newton centroid while still counting every root). Retaining the doubled stored square (half-width 2·2^{−prec} ≥ the disc radius √2·2^{−prec}) restores the cover for both certificate forms, at the cost of one precision level, which the strictly-finer adoption guard in isolateLoop still absorbs (a Newton jump gains at least two levels).

Equations

• (Hex.Certified.atom iso).toComponent = { squares := #[iso.square.doubled], candidateK := 1 }
• (Hex.Certified.cluster cl).toComponent = { squares := #[(Hex.encSquare cl.squares).doubled], candidateK := cl.k }

def Hex.pairwiseDisjoint (ss : Array DyadicSquare) : Bool

All stored squares' circumscribed discs are pairwise disjoint, i.e. !discsMeet holds for every pair. One exact dyadic comparison per pair, as in the SimpleRoot intersection test.

Equations

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

def Hex.fuelFor (p : ZPoly) (target start : Int) : Nat

Fuel for isolateLoop: the laggard's climb from the worklist's coarsest prec to stopDepth, plus a second climb from target to stopDepth for a held component forced back into refinement by a late-certifying overlapping sibling (see isolateLoop).

Equations

• Hex.fuelFor p target start = (Hex.stopDepth p target - start).toNat + (Hex.stopDepth p target - target).toNat + 1

def Hex.IsolationLoop.normalized (p : ZPoly) (target : Int) (tried : Array (Component × Option (Certified p))) : Bool

Every component has reached the globally normalized completeness depth.

Equations

• Hex.IsolationLoop.normalized p target tried = tried.all fun (t : Hex.Component × Option (Hex.Certified p)) => decide (Hex.completenessDepth p target ≤ t.fst.prec)

def Hex.IsolationLoop.attempts (p : ZPoly) (strategy : AtomStrategy) (work : Array Component) : Array (Component × Option (Certified p))

Attempt certification on every component in a worklist.

Equations

• Hex.IsolationLoop.attempts p strategy work = Array.map (fun (c : Hex.Component) => (c, Hex.Component.certify? p strategy c)) work

def Hex.IsolationLoop.allReady {p : ZPoly} (target : Int) (tried : Array (Component × Option (Certified p))) : Bool

Every attempted component certified at the requested stored precision.

Equations

• Hex.IsolationLoop.allReady target tried = tried.all fun (t : Hex.Component × Option (Hex.Certified p)) => match t.snd with | some r => decide (target ≤ r.square.prec) | none => false

def Hex.IsolationLoop.outputs {p : ZPoly} (tried : Array (Component × Option (Certified p))) : Array (Certified p)

The successful certificates in an attempts array.

Equations

• Hex.IsolationLoop.outputs tried = Array.filterMap (fun (x : Hex.Component × Option (Hex.Certified p)) => x.snd) tried

def Hex.IsolationLoop.allAtoms {p : ZPoly} (tried : Array (Component × Option (Certified p))) : Bool

Every attempted component certified as an atom. This stronger form is also the guard for leaving global reglue early: failures and cluster results must remain in the globally normalized subdivision path.

Equations

• Hex.IsolationLoop.allAtoms tried = tried.all fun (t : Hex.Component × Option (Hex.Certified p)) => match t.snd with | some (Hex.Certified.atom iso) => true | x => false

def Hex.IsolationLoop.disjoint {p : ZPoly} (tried : Array (Component × Option (Certified p))) : Bool

The stored squares of successful attempts are pairwise disjoint.

Equations

• Hex.IsolationLoop.disjoint tried = Hex.pairwiseDisjoint (Array.map (fun (x : Hex.Certified p) => x.square) (Hex.IsolationLoop.outputs tried))

def Hex.IsolationLoop.overlaps {p : ZPoly} (tried : Array (Component × Option (Certified p))) (i : Nat) (res : Certified p) : Bool

Whether a successful result overlaps another successful result in the attempts array.

Equations

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

def Hex.IsolationLoop.step (p : ZPoly) (target : Int) (tried : Array (Component × Option (Certified p))) (i : Nat) : Array Component

The contribution of one attempted component to a non-emitting round.

Equations

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

def Hex.IsolationLoop.nextLocal (p : ZPoly) (target : Int) (tried : Array (Component × Option (Certified p))) : Array Component

Worklist for a non-emitting round. Ready certificates disjoint from all other successful certificates hold their input component; other successes adopt a strictly finer doubled result or refine, and failures refine.

Equations

• Hex.IsolationLoop.nextLocal p target tried = Array.flatMap (Hex.IsolationLoop.step p target tried) (Array.range tried.size)

def Hex.IsolationLoop.next (p : ZPoly) (target : Int) (tried : Array (Component × Option (Certified p))) : Array Component

Worklist for a non-emitting full-isolation round. Before normalization, all squares refine and reglue globally; afterwards this is nextLocal.

Equations

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

def Hex.refineLoop (p : ZPoly) (target : Int) (strategy : AtomStrategy) : Nat → Array Component → Option (Array (Certified p))

Refinement loop for one already-isolated atom. Bisection can split even one starting component into several surviving pieces, so up to the fixed completeness depth this re-splits and re-merges components exactly as the full driver does. A result is emitted only when it is the single atom at the target precision that refineAtom? requires.

Equations

• One or more equations did not get rendered due to their size.
• Hex.refineLoop p target strategy 0 x✝ = none

def Hex.fastRefineFuel : Nat

Budget for the fast lineage-local pass, tried before the full driver. A successful Newton adoption normally needs only logarithmically many rounds; failure just restarts from the original atom on refineLoop.

Equations

• Hex.fastRefineFuel = 64

def Hex.refineFastLoop (p : ZPoly) (target : Int) (strategy : AtomStrategy) : Nat → Array Component → Option (Array (Certified p))

Opportunistic refinement along one atom's lineage. This loop is only a fast path: its result is accepted under the same singleton-atom guard as refineLoop, and any failure falls back to the full driver, which re-splits and re-merges components across the whole search.

Equations

• One or more equations did not get rendered due to their size.
• Hex.refineFastLoop p target strategy 0 x✝ = none

def Hex.refineFastAtom? {p : ZPoly} (iso : DyadicRootIsolation p) (target : Int) (strategy : AtomStrategy) : Option (DyadicRootIsolation p)

Bounded speculative refinement of one atom. A rejected or exhausted run returns none, so callers can fall back without trusting this optimization.

Equations

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

def Hex.refineAtom? {p : ZPoly} (iso : DyadicRootIsolation p) (target : Int) (strategy : AtomStrategy) : Option (DyadicRootIsolation p)

Atom refiner shared by the local one-root search and the all-atoms fast path in the full isolation driver.

Equations

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

def Hex.firstRefinedAtom? {p : ZPoly} (target : Int) (strategy : AtomStrategy) (tried : Array (Component × Option (Certified p))) : Option (DyadicRootIsolation p)

Find and refine the first atom among a round's certification attempts. Array order makes the choice deterministic; clusters, failed certifications, and atoms that fail to refine are skipped.

Equations

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

def Hex.nextAtomSearch {p : ZPoly} (tried : Array (Component × Option (Certified p))) : Array Component

Refine every component of a one-atom search round. A certified cluster is re-entered through its tighter certified region when that makes progress; otherwise it, and every failed component, is subdivided locally.

Equations

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

def Hex.findAtomLoop (p : ZPoly) (target : Int) (strategy : AtomStrategy) : Nat → Array Component → Option (DyadicRootIsolation p)

Search a caller-selected region for one certified simple root, then refine that atom to target. Unlike isolateLoop, this loop does not construct a complete, pairwise-disjoint family: an atom certificate already states that its own region contains exactly one simple root. Consequently a successful result is sound without examining or refining any other root. none means the region was exhausted or no atom was found within fuel.

Equations

• One or more equations did not get rendered due to their size.
• Hex.findAtomLoop p target strategy 0 x✝ = none

def Hex.IsolationLoop.refineAttempt? {p : ZPoly} (target : Int) (strategy : AtomStrategy) (t : Component × Option (Certified p)) : Option (DyadicRootIsolation p)

Refine the atom returned by one successful component attempt. Use the bounded lineage-local loop first, then fall back to complete normalized refinement when the local attempt cannot finish.

Equations

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

def Hex.IsolationLoop.finishAllAtoms? (p : ZPoly) (target : Int) (strategy : AtomStrategy) (tried : Array (Component × Option (Certified p))) : Option (Array (Certified p))

Strategy-parametric implementation of the all-atoms finishing pass.

Equations

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

def Hex.IsolationLoop.finishAtoms? (p : ZPoly) (target : Int) (strategy : AtomStrategy) (tried : Array (Component × Option (Certified p))) : Option (Array (Certified p))

Opportunistically refine every successful atom to the requested target. The nested work starts only when every attempt is an atom and the current discs are pairwise disjoint; the result is accepted only when every local refinement succeeds and the refined discs remain pairwise disjoint. The NK-only strategy keeps its existing proof-specialized loop path.

Equations

• Hex.IsolationLoop.finishAtoms? p target Hex.AtomStrategy.nk tried = none
• Hex.IsolationLoop.finishAtoms? p target Hex.AtomStrategy.pellet tried = Hex.IsolationLoop.finishAllAtoms? p target Hex.AtomStrategy.pellet tried
• Hex.IsolationLoop.finishAtoms? p target Hex.AtomStrategy.nkThenPellet tried = Hex.IsolationLoop.finishAllAtoms? p target Hex.AtomStrategy.nkThenPellet tried

def Hex.IsolationLoop.emitReady {p : ZPoly} (target : Int) (strategy : AtomStrategy) (tried : Array (Component × Option (Certified p))) : Bool

Ordinary output guard after the optional local finisher. Normalized worklists may emit any ready, disjoint certificates. The NK-only strategy also retains its historical early all-atoms emission; Pellet-bearing strategies use the stronger local finisher above.

Equations

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

def Hex.isolateLoop (p : ZPoly) (target : Int) (strategy : AtomStrategy) : Nat → Array Component → Option (Array (Certified p))

The shared driver loop over the worklist. It may emit before completenessDepth when every result is already an atom and target-ready, with pairwise-disjoint discs. Before that depth, every non-emitting round globally refines and reglues the retained squares, irrespective of attempted certificates. At and beyond that depth, ready and disjoint cluster results may emit too. Otherwise: a component already certified at target whose disc is disjoint from every other certified disc holds its position; every other surviving component subdivides one level, except that one adopting a strictly finer certified result keeps that result as a one-square component instead. Each post-normalization non-emitting round strictly increases every non-held component's prec, and held components sit at target, so the laggard's prec reaches stopDepth within (stopDepth − min prec) rounds. A held component can be forced back into refinement late, when a slow sibling finally certifies with an overlapping disc, so fuelFor budgets a second climb on top: past separationDepth every certified disc is below sep/4 and distinct roots' discs are disjoint, so (stopDepth − target) further rounds suffice. fuel = 0 returns none (up to a harmless constant of overshoot). The recursion is structural on the fuel Nat.

Equations

• One or more equations did not get rendered due to their size.
• Hex.isolateLoop p target strategy 0 x✝ = none

def Hex.DyadicRootIsolation.refineTo? {p : ZPoly} (iso : DyadicRootIsolation p) (target : Int) (strategy : AtomStrategy := AtomStrategy.nkThenPellet) : Option (DyadicRootIsolation p)

Refine to target precision. A bounded pass along the atom's own lineage keeps the usual Newton path, which roughly doubles the correct bits per step. If that pass does not produce exactly one atom at the target precision, refinement starts again from the input under the full driver, which re-splits and re-merges components across the whole search.

Equations

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