structure Hex.RCF.IsolationCert : Type

Raw intervals proposed as an ordered, complete isolation of the roots of the head polynomial of a generalized Sturm replay.

• intervals : Array DyadicInterval

  Proposed half-open root intervals in ascending order.

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

Check that every supplied interval has literal replay count one.

Equations

• Hex.RCF.IsolationCert.checkCounts replay cert = (List.range cert.intervals.size).all fun (i : Nat) => if h : i < cert.intervals.size then decide (replay.count cert.intervals[i] = 1) else false

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

Check the emitted order in linear time using only adjacent pairs. This is intentionally non-strict for half-open isolations. Strict gaps are checked by the later cell-separation certificate.

Equations

• cert.checkOrder = (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.check (replay : SturmReplay) (cert : IsolationCert) : Bool

Validate literal interval counts, ordering, and total completeness. Replay validation is a separate premise so an outer checker need not reduce it twice.

Equations

• Hex.RCF.IsolationCert.check replay cert = (Hex.RCF.IsolationCert.checkCounts replay cert && cert.checkOrder && decide (replay.total = ↑cert.intervals.size))

theorem Hex.RCF.IsolationCert.count_one_of_check {replay : SturmReplay} {cert : IsolationCert} (h : checkCounts replay cert = true) (i : Fin cert.intervals.size) : replay.count cert.intervals[i] = 1

Every interval accepted by the count walk has literal count one.

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

Each adjacent interval pair accepted by the order walk is separated in the non-strict half-open sense.

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

Adjacent ordering implies the all-pairs ordering used by the semantic literal-isolation layer.

theorem Hex.RCF.IsolationCert.complete_of_check {replay : SturmReplay} {cert : IsolationCert} (h : check replay cert = true) : replay.total = ↑cert.intervals.size

The completeness equality recovered from the Boolean isolation checker.

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

The count component recovered from the combined checker.

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

The order component recovered from the combined checker.