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)

The actual count splitter installs all constant-count run indices and preserves cache entries outside the original cell.