def Hex.RefinedRealIsolation (p : ZPoly) : Type

An isolation refined to separation precision: its interval has width at most 2^{−sepPrec p}. At width below sep(p)/4, two refined isolations isolate the same root exactly when their intervals overlap.

Equations

• Hex.RefinedRealIsolation p = { iso : Hex.RealRootIsolation p // iso.interval.upper - iso.interval.lower ≤ Hex.twoPow (-↑(Hex.sepPrec p)) }

def Hex.Overlaps {p : ZPoly} (i₁ i₂ : RefinedRealIsolation p) : Prop

The half-open intervals of two refined isolations intersect: max lower₁ lower₂ < min upper₁ upper₂. Core Dyadic has no Min/Max instance, so the max and min are written with explicit ifs; the whole test is a single dyadic comparison at runtime.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.instDecidableOverlaps {p : ZPoly} (i₁ i₂ : RefinedRealIsolation p) : Decidable (Overlaps i₁ i₂)

Equations

• Hex.instDecidableOverlaps i₁ i₂ = Hex.instDecidableOverlaps._aux_1 i₁ i₂

def Hex.SimpleRealRoot (p : ZPoly) : Type

The identity of a real root, independent of which isolation witnessed it: the quotient of refined isolations by interval overlap.

Equations

• Hex.SimpleRealRoot p = Quot Hex.Overlaps

def Hex.SimpleRealRoot.mk {p : ZPoly} (iso : RefinedRealIsolation p) : SimpleRealRoot p

Package a refined isolation as a root identity.

Equations

• Hex.SimpleRealRoot.mk iso = Quot.mk Hex.Overlaps iso

def Hex.RefinedRealIsolation.sameRoot {p : ZPoly} (i₁ i₂ : RefinedRealIsolation p) : Bool

Boolean form of Overlaps, used for equality tests on data containing roots. The companion proves it decides equality in SimpleRealRoot p.

Equations

• i₁.sameRoot i₂ = decide (Hex.Overlaps i₁ i₂)

def Hex.RealRootIsolation.refined {p : ZPoly} (iso : RealRootIsolation p) : Option (RefinedRealIsolation p)

Refine an isolation to separation precision and package it as a RefinedRealIsolation. Refinement runs refineTo (sepPrec p); the width test that follows is some on any honest isolation of a squarefree p (the companion's refine1_isolates_same shows refineTo actually shrinks below 2^{−sepPrec p}, so the none branch is unreachable there). It is Option only because on junk data violating the isolation semantics refineTo can return its input unshrunk. This is the obvious producer the threading pattern needs: call it once, then thread the refined value forward.

Equations

• One or more equations did not get rendered due to their size.