theorem Hex.GraphIso.Nauty.Sparse.splitCounts_queue {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hb : s.cellend[first]! < n) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (hq : CellQueue s.ptn level s.active s.queue) : have t := splitCounts level first distance s; CellQueue t.ptn level t.active t.queue

The executed count splitter preserves the exact active queue, including its largest-fragment replacement and bounded tail scan.