structure Hex.GraphIso.Nauty.Sparse.CountTrace.Ready {n : Nat} (level : Nat) (key : Nat → Nat) (first last : Nat) (s : RefineSt n) : Prop

A pending count cell retains its original endpoints and exact semantic counts until its turn in the native touched-cell loop.

• cell : IsCell s.ptn level first (last + 1 - first)
• le : first ≤ last
• bound : last < n
• keys (q : Nat) : first ≤ q → q ≤ last → s.hits[s.lab[q]!]! < n + 2
• values (v : Nat) : v ∈ segN s.lab first (last + 1 - first) → s.hits[v]! = key v

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Ready.endpoint {n level : Nat} {key : Nat → Nat} {first last : Nat} {s : RefineSt n} (h : Ready level key first last s) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) : s.cellend[first]! = last

Valid endpoint caches agree with the original pending cell.

theorem Hex.GraphIso.Nauty.Sparse.CountTrace.Ready.keep {n level : Nat} {key : Nat → Nat} {first last a b : Nat} {s : RefineSt n} (h : Ready level key first last s) (other : Ready level key a b s) (hne : a ≠ first) (distance : Bool) (hp : s.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) : Ready level key a b (splitCounts level first distance s)

Processing a different cell leaves pending cell keys and their exact semantic values intact, as well as its partition boundaries.