HexRootsMathlib.Refinement

source

theorem HexRootsMathlib.DyadicRootIsolation.refineTo_root {p : Hex.ZPoly} (iso : Hex.DyadicRootIsolation p) (target : ℤ) (strategy : Hex.AtomStrategy) {iso' : Hex.DyadicRootIsolation p} (hrun : iso.refineTo? target strategy = some iso') :

root iso' = root iso

Refining an atom certificate preserves its selected complex root.

source

theorem HexRootsMathlib.DyadicRootIsolation.refineTo_ready {p : Hex.ZPoly} {iso iso' : Hex.DyadicRootIsolation p} {target : ℤ} {strategy : Hex.AtomStrategy} (hrun : iso.refineTo? target strategy = some iso') :

target ≤ iso'.square.prec

Every successful raw refinement result reaches its requested precision.

source

theorem HexRootsMathlib.RefinedIsolation.refineTo_root {p : Hex.ZPoly} (r : Hex.RefinedIsolation p) (target : ℤ) (strategy : Hex.AtomStrategy) {out : { r' : Hex.RefinedIsolation p // Hex.SimpleRoot.mk r' = Hex.SimpleRoot.mk r }} (hrun : r.refineTo? target strategy = some out) :

root ↑out = root r

Refined-level refinement preserves the semantic root represented by the returned subtype. This operational result is unconditional: it follows from the successful raw refinement call, independently of quotient semantics.