def Hex.RCF.IsolationCert.checkGaps (cert : IsolationCert) : Bool

Check strict gaps between every adjacent pair of emitted intervals.

Equations

• cert.checkGaps = (List.range (cert.intervals.size - 1)).all fun (i : Nat) => if h : i + 1 < cert.intervals.size then decide (cert.intervals[i].upper < cert.intervals[i + 1].lower) else false

def Hex.RCF.IsolationCert.checkStrict (replay : SturmReplay) (cert : IsolationCert) : Bool

Validate generalized isolation and strict adjacent separation.

Equations

• Hex.RCF.IsolationCert.checkStrict replay cert = (Hex.RCF.IsolationCert.check replay cert && cert.checkGaps)

theorem Hex.RCF.IsolationCert.check_of_checkStrict {replay : SturmReplay} {cert : IsolationCert} (h : checkStrict replay cert = true) : check replay cert = true

Recover the underlying generalized isolation check.

theorem Hex.RCF.IsolationCert.gaps_of_checkStrict {replay : SturmReplay} {cert : IsolationCert} (h : checkStrict replay cert = true) : cert.checkGaps = true

Strict validation exposes its strict-gap component.

theorem Hex.RCF.IsolationCert.gap_of_check {cert : IsolationCert} (h : cert.checkGaps = true) (i : Nat) (hi : i + 1 < cert.intervals.size) : cert.intervals[i].upper < cert.intervals[i + 1].lower

Every adjacent pair accepted by the strict-gap walk is strictly separated.

theorem Hex.RCF.IsolationCert.gaps_of_check {cert : IsolationCert} (h : cert.checkGaps = true) (i j : Fin cert.intervals.size) : i < j → cert.intervals[i].upper < cert.intervals[j].lower

Strict adjacent gaps imply strict separation for every earlier/later pair.

inductive Hex.RCF.Separation.RootCmp : Type

The order of an isolated real root relative to an exact dyadic endpoint.

• lt : RootCmp

  The isolated root is strictly below the endpoint.

• eq : RootCmp

  The isolated root equals the endpoint.

• gt : RootCmp

  The endpoint is strictly below the isolated root.

@[instance_reducible]

instance Hex.RCF.Separation.instDecidableEqRootCmp : DecidableEq RootCmp

Equations

• Hex.RCF.Separation.instDecidableEqRootCmp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hex.RCF.Separation.instReprRootCmp.repr : RootCmp → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.RCF.Separation.instReprRootCmp : Repr RootCmp

Equations

• Hex.RCF.Separation.instReprRootCmp = { reprPrec := Hex.RCF.Separation.instReprRootCmp.repr }

def Hex.RCF.Separation.classify? (f : ZPoly) (replay : SturmReplay) (I : DyadicInterval) (endpoint : Dyadic) : Option RootCmp

Classify one isolated root against an exact dyadic endpoint. In the interior case, the literal replay count on the prefix interval determines the side, with exact polynomial evaluation resolving equality.

Equations

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

def Hex.RCF.Separation.checkCmp (f : ZPoly) (replay : SturmReplay) (I : DyadicInterval) (endpoint : Dyadic) (claim : RootCmp) : Bool

Recompute and check a claimed endpoint comparison. Sound use additionally requires the outer certificate to establish replay.check f.

Equations

• Hex.RCF.Separation.checkCmp f replay I endpoint claim = decide (Hex.RCF.Separation.classify? f replay I endpoint = some claim)

def Hex.RCF.Separation.refine1? (replay : SturmReplay) (I : DyadicInterval) : Option DyadicInterval

Bisect one raw interval and retain a count-one half. The midpoint variation is shared between the two candidate counts.

Equations

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

def Hex.RCF.Separation.refinePairWith? (replay : SturmReplay) : Nat → DyadicInterval → DyadicInterval → Option (DyadicInterval × DyadicInterval)

Separate a pair with an explicit structural fuel budget.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RCF.Separation.refinePairWith? replay 0 x✝¹ x✝ = if x✝¹.upper < x✝.lower then some (x✝¹, x✝) else if x✝¹.upper ≤ x✝.lower then none else none

def Hex.RCF.Separation.refinePair? (p : ZPoly) (replay : SturmReplay) (left right : DyadicInterval) : Option (DyadicInterval × DyadicInterval)

Refine both members of a touching pair until they have a strict gap or the structural fuel is exhausted. Genuine overlaps and malformed count data are rejected.

Equations

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

def Hex.RCF.Separation.separateFrom? (p : ZPoly) (replay : SturmReplay) (previous : DyadicInterval) : List DyadicInterval → Option (List DyadicInterval)

Continue a left-to-right separation scan from its current interval.

Equations

• One or more equations did not get rendered due to their size.
• Hex.RCF.Separation.separateFrom? p replay previous [] = some [previous]

def Hex.RCF.Separation.separateList? (p : ZPoly) (replay : SturmReplay) : List DyadicInterval → Option (List DyadicInterval)

Left-to-right separation scan. Refining a later interval only shrinks it, so honest input preserves every strict gap already emitted.

Equations

• Hex.RCF.Separation.separateList? p replay [] = some []
• Hex.RCF.Separation.separateList? p replay (next :: rest) = Hex.RCF.Separation.separateFrom? p replay next rest

def Hex.RCF.Separation.separate? (p : ZPoly) (replay : SturmReplay) (cert : IsolationCert) : Option IsolationCert

Run untrusted strict separation and retain only checker-approved output. The caller pairs p with a replay checked against it. A mismatch can only choose inadequate fuel and make this builder return none, because the output checker reads counts solely from replay.

Equations

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

theorem Hex.RCF.Separation.check_separate {p : ZPoly} {replay : SturmReplay} {input output : IsolationCert} (h : separate? p replay input = some output) : IsolationCert.checkStrict replay output = true

The public builder never returns an unchecked strict isolation array.