theorem Hex.GraphIso.Nauty.Sparse.splitCounts_invariant {n : Nat} (level first last : Nat) (distance : Bool) (s t : RefineSt n) (hsl : s.lab.toList.Perm (List.range n)) (htl : t.lab.toList.Perm (List.range n)) (hsp : s.ptn.size = n) (htp : t.ptn = s.ptn) (hh : t.hits = s.hits) (hse : s.cellend[first]! = last) (hte : t.cellend[first]! = last) (hf : first ≤ last) (hb : last < n) (hsk : ∀ (q : Nat), first ≤ q → q ≤ last → s.hits[s.lab[q]!]! < n + 2) (htk : ∀ (q : Nat), first ≤ q → q ≤ last → t.hits[t.lab[q]!]! < n + 2) (hc : IsCell s.ptn level first (last + 1 - first)) (hp : cellsPerm s.ptn level s.lab t.lab) : (splitCounts level first distance s).ptn = (splitCounts level first distance t).ptn ∧ cellsPerm (splitCounts level first distance s).ptn level (splitCounts level first distance s).lab (splitCounts level first distance t).lab

Permuting vertices within input cells does not change the ordered count classes produced by the optimized count splitter.