theorem Hex.Interval.bounds {p : ZPoly} (a : RefinedIsolation p) : (HexRootsMathlib.Dyadic.toReal ((↑a).square.re - (↑a).square.radiusHi) ≤ a.root.re ∧ a.root.re ≤ HexRootsMathlib.Dyadic.toReal ((↑a).square.re + (↑a).square.radiusHi)) ∧ HexRootsMathlib.Dyadic.toReal ((↑a).square.im - (↑a).square.radiusHi) ≤ a.root.im ∧ a.root.im ≤ HexRootsMathlib.Dyadic.toReal ((↑a).square.im + (↑a).square.radiusHi)

Both coordinate projections lie in the dyadic radius bounds.

theorem Hex.Interval.realOrder?_sound {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q) {o : Ordering} (h : realOrder? (↑a).square (↑b).square = some o) : compare a.root.re b.root.re = o

A disjoint real interval comparison agrees with comparison of the real values.

theorem Hex.Interval.imagApart_sound {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q) (h : imagApart (↑a).square (↑b).square = true) : a.root.im ≠ b.root.im

Separated imaginary intervals cannot have equal imaginary coordinates.

theorem Hex.Interval.notLt_sound {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q) (h : notLt (↑a).square (↑b).square = true) : ¬a.root.re < b.root.re

A strict-order rejection is sound.

theorem Hex.Interval.notLe_sound {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q) (h : notLe (↑a).square (↑b).square = true) : ¬a.root.re ≤ b.root.re

A non-strict-order rejection is sound.

theorem Hex.Interval.search_sound {α : Type} (probe : DyadicSquare → DyadicSquare → Option α) (R : ℂ → ℂ → α → Prop) (sound : ∀ {p q : ZPoly} (a : RefinedIsolation p) (b : RefinedIsolation q) (v : α), probe (↑a).square (↑b).square = some v → R a.root b.root v) {p q : ZPoly} (targets : List (ℤ × ℤ)) (a : RefinedIsolation p) (b : RefinedIsolation q) {v : α} (h : search probe targets a b = some v) : R a.root b.root v

Threaded refinement preserves any sound coordinate probe.