9.5. Refining a root🔗

The precision the driver reaches is only as fine as separating the roots required, floored at the target. To sharpen a single root without re-running the whole isolator, refine its atom directly:

def

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

Refine to target precision. A bounded lineage-local pass preserves the usual logarithmic speculative-Newton path. If it does not produce exactly one target-ready atom, refinement restarts from the input under the globally reglued complete loop.

Refinement combines a speculative Newton step, which gains quadratic precision when it certifies, with subdivision as the fallback. It preserves the root, so the refined atom can stand in for the original wherever a caller needs a tighter enclosure. This is the operation the demo uses to drive the real root of x³ − x − 1 down to 80 bits.

For consumers that need to compare roots for identity rather than approximate them, an atom refined to at least separation precision can be wrapped as a Hex.RefinedIsolation through Hex.DyadicRootIsolation.toRefined?, and Hex.RefinedIsolation.sameRoot then decides whether two such isolations name the same root by a single dyadic disc-intersection test. hex-number-field builds on that comparison.