theorem Hex.GraphIso.Nauty.Sparse.splitCounts_index {n : Nat} (level first len : Nat) (distance : Bool) (s : RefineSt n) (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) (hc : IsCell s.ptn level first len) (hb : first + len ≤ n) (hk : ∀ (q : Nat), first ≤ q → q < first + len → s.hits[s.lab[q]!]! < n + 2) : have t := splitCounts level first distance s; Index.Valid n t.lab t.ptn level t.cellstart t.cellend

Count splitting preserves a valid partition index. The cache supplies the executed endpoint and the original vertex indices; callers need only identify the bounded cell and supply the local hit bound.