Documentation

HexRCF.Separation

source
theorem Hex.RCF.IsolationCert.roots_lt_of_check {cert : IsolationCert} (h : cert.checkGaps = true) {i j : Fin cert.intervals.size} (hij : i < j) {ri rj : ℝ} (hi : HexRealRootsMathlib.Literal.InInterval cert.intervals[i] ri) (hj : HexRealRootsMathlib.Literal.InInterval cert.intervals[j] rj) :
ri < rj

Strictly separated intervals contain roots in the corresponding strict order.

source
def Hex.RCF.Separation.RootCmp.Holds :
RootCmp → ℝ → ℝ → Prop

Semantic interpretation of an endpoint comparison.

Equations
Instances For
    source
    theorem Hex.RCF.Separation.classify_sound {f : ZPoly} {replay : SturmReplay} {cert : IsolationCert} (hreplay : SturmReplay.check f replay = true) (hcert : IsolationCert.check replay cert = true) (i : Fin cert.intervals.size) (endpoint : Dyadic) {cmp : RootCmp} (hcmp : classify? f replay cert.intervals[i] endpoint = some cmp) :
    ∃! root : ℝ, (HexRealRootsMathlib.toPolyℝ f).IsRoot root ∧ HexRealRootsMathlib.Literal.InInterval cert.intervals[i] root ∧ cmp.Holds root (HexRealRootsMathlib.Dyadic.toReal endpoint)

    Every successful endpoint classification has the stated order against the unique root in the accepted isolation.

    source
    theorem Hex.RCF.Separation.classify_exists {f : ZPoly} {replay : SturmReplay} {cert : IsolationCert} (hreplay : SturmReplay.check f replay = true) (hcert : IsolationCert.check replay cert = true) (i : Fin cert.intervals.size) (endpoint : Dyadic) :
    ∃ (cmp : RootCmp), classify? f replay cert.intervals[i] endpoint = some cmp

    Valid replay isolations classify every dyadic endpoint: the interior prefix count cannot exceed the count-one enclosing interval.

    source
    theorem Hex.RCF.Separation.checkCmp_sound {f : ZPoly} {replay : SturmReplay} {cert : IsolationCert} (hreplay : SturmReplay.check f replay = true) (hcert : IsolationCert.check replay cert = true) (i : Fin cert.intervals.size) (endpoint : Dyadic) (claim : RootCmp) (hclaim : checkCmp f replay cert.intervals[i] endpoint claim = true) :
    ∃! root : ℝ, (HexRealRootsMathlib.toPolyℝ f).IsRoot root ∧ HexRealRootsMathlib.Literal.InInterval cert.intervals[i] root ∧ claim.Holds root (HexRealRootsMathlib.Dyadic.toReal endpoint)

    A checked comparison claim inherits the classifier soundness theorem.