theorem Hex.GraphIso.Nauty.Sparse.CountSort.finish_cache {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (lab : Array Nat) (w1 v2 w2 v3 : Nat) (hp : s.lab.toList.Perm (List.range n)) (hs : s.cellstart.size = n) (he : s.cellend.size = n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < n) (hc : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.cellstart[s.lab[q]!]! = if first = s.cellend[first]! then n else first) (hm : Minima.Permuted s.lab lab s.hits first (s.cellend[first]! + 1) v2 v3 (s.cellend[first]! + 1) w1 w2 (n + 2)) : Index.Complete n first s.cellend[first]! s.lab s.hits s.cellstart s.cellend (finish level first (s.cellend[first]! + 1) distance { lab := lab, ptn := s.ptn, active := s.active, queue := s.queue, cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode } w1 v2 w2 v3)

Fragment installation indexes every constant-count run and preserves cache entries outside the original cell.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_cache {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hs : s.cellstart.size = n) (he : s.cellend.size = n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < n) (hc : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.cellstart[s.lab[q]!]! = if first = s.cellend[first]! then n else first) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) : Index.Complete n first s.cellend[first]! s.lab s.hits s.cellstart s.cellend (splitCounts level first distance s)

Count splitting installs all constant-count run indices and preserves the cache outside its original cell.