theorem Hex.GraphIso.Nauty.Sparse.splitCounts_partition {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) : CountPartition level first s.cellend[first]! (splitCounts level first distance s).lab s.hits s.ptn (splitCounts level first distance s).ptn

The executed count splitter closes exactly the boundaries between unequal adjacent counts inside the original cell, retaining every other value.