def Hex.RealRootIsolation.refine1With {p : ZPoly} (chain : Array ZPoly) (hchain : chain = p.sturmChain) (iso : RealRootIsolation p) : RealRootIsolation p

Bisect an isolation at its dyadic midpoint and keep the half whose Sturm count is 1.

One chain construction, then at most four endpoint evaluations decide it: the midpoint m is (lower + upper) / 2 computed exactly, so a genuine interval always splits into two nonempty halves. The left half (lower, m] is tried first — its Sturm count is sturmVarAt chain lower − sturmVarAt chain m, phrased directly on the let-bound chain so the chain is built once, never per ZPoly.sturmCount. If the left count is 1 it certifies; otherwise the right half (m, upper] is tried the same way. The half-open convention means a root exactly at m lands in the left half (lower, m] and its count is 1 there, so no endpoint comparison against m is ever needed.

If neither half certifies — impossible for squarefree p, proven unreachable by the companion refine1_isolates_same — the input is returned unchanged, so the function is total.

The bisection logic is factored into refine1With, which takes an already-built chain; refine1 supplies ZPoly.sturmChain p (rebuilt per call, matching its fixed signature), while callers refining many levels thread one chain through refineToWithChain.

Equations

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

def Hex.RealRootIsolation.refine1 {p : ZPoly} (iso : RealRootIsolation p) : RealRootIsolation p

Bisect an isolation at its dyadic midpoint and keep the half whose Sturm count is 1. See refine1With for the mechanism; this rebuilds the Sturm chain each call.

Equations

• iso.refine1 = Hex.RealRootIsolation.refine1With p.sturmChain ⋯ iso

def Hex.RealRootIsolation.refineToWithChain {p : ZPoly} (chain : Array ZPoly) (hchain : chain = p.sturmChain) (iso : RealRootIsolation p) (target : Int) : RealRootIsolation p

Cached-chain refinement: iterate refine1With against one precomputed chain until the interval width is at most 2^{−target}.

Identical semantics to refineTo, but the Sturm chain is built once for the whole descent rather than rebuilt at every bisection level — the memoisation the isolate_roots elaborator needs when refining every root to a requested width. The fuel is (ceilLog2Dyadic width + target).toNat + 1, exactly as refineTo.

Equations

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

def Hex.RealRootIsolation.refineTo {p : ZPoly} (iso : RealRootIsolation p) (target : Int) : RealRootIsolation p

Iterate refine1 until the interval width is at most 2^{−target}.

The fuel is (ceilLog2Dyadic width + target).toNat + 1. Since width ≤ 2^{ceilLog2Dyadic width} and each honest refine1 halves the width, ceilLog2Dyadic width + target halvings bring the width to at most 2^{−target}; the .toNat clamps the already-satisfied case (a nonpositive gap) to 0, and the + 1 covers the loop's own width test. On adversarial data that violates the isolation semantics refine1 returns its input, and the loop then drains its fuel without shrinking — total either way, it cannot loop.

Delegates to refineToWithChain with chain = ZPoly.sturmChain p, so the whole descent shares one chain construction.

Equations

• iso.refineTo target = Hex.RealRootIsolation.refineToWithChain p.sturmChain ⋯ iso target