12.5. Refining a root🔗

The precision the driver reaches is only as fine as separating the roots required, with the target as a lower bound. 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 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.

Refinement first tries a Newton step, which roughly doubles the number of correct bits each time it certifies. When the step does not certify, the square is bisected and the search continues on the halves, which is slower but always makes progress. Either way the root is preserved, 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.