def Hex.Interval.realOrder? (a b : DyadicSquare) : Option Ordering

Strict ordering certified by disjoint real-coordinate intervals.

Equations

• Hex.Interval.realOrder? a b = if a.re + a.radiusHi < b.re - b.radiusHi then some Ordering.lt else if b.re + b.radiusHi < a.re - a.radiusHi then some Ordering.gt else none

def Hex.Interval.imagApart (a b : DyadicSquare) : Bool

Disjoint imaginary-coordinate intervals certify incomparability.

Equations

• Hex.Interval.imagApart a b = (decide (a.im + a.radiusHi < b.im - b.radiusHi) || decide (b.im + b.radiusHi < a.im - a.radiusHi))

def Hex.Interval.notLt (a b : DyadicSquare) : Bool

A sound rejection of strict real-coordinate order, including touching endpoints.

Equations

• Hex.Interval.notLt a b = decide (b.re + b.radiusHi ≤ a.re - a.radiusHi)

def Hex.Interval.notLe (a b : DyadicSquare) : Bool

A sound rejection of non-strict real-coordinate order.

Equations

• Hex.Interval.notLe a b = decide (b.re + b.radiusHi < a.re - a.radiusHi)

def Hex.Interval.search {α : Type} {p q : ZPoly} (probe : DyadicSquare → DyadicSquare → Option α) : List (Int × Int) → RefinedIsolation p → RefinedIsolation q → Option α

Probe stored squares first, then thread both representatives through a finite schedule. none means inconclusive or failed refinement, never mathematical incomparability.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Interval.search probe [] x✝¹ x✝ = match probe x✝¹.val.square x✝.val.square with | some result => some result | none => none

def Hex.Interval.targets (cap : Int) : Nat → Int → List (Int × Int)

Geometrically increasing targets, capped and structurally fueled.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Interval.targets cap 0 x✝ = []

def Hex.Interval.extra (a b : DyadicSquare) : List (Int × Int)

Two modest extra-precision rounds for an otherwise exact fallback.

Equations

• Hex.Interval.extra a b = [(a.prec + 16, b.prec + 16), (a.prec + 64, b.prec + 64)]