theorem Hex.GraphIso.Nauty.Sparse.CountSort.finish_sorted {n : Nat} (level first last : Nat) (distance : Bool) (s : RefineSt n) (w1 v2 w2 v3 : Nat) (h : Minima s.lab s.hits first v2 v3 last w1 w2) (hb : last ≤ s.lab.size) : «Sort».Sorted (finish level first last distance s w1 v2 w2 v3).lab s.hits first (last - first)

Installing the minimum-count fragments and sorting their tail orders the entire cell. Index, queue and hash updates preserve that label array.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_sorted {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < s.lab.size) (hk : s.hits[s.lab[first]!]! < n + 2) : «Sort».Sorted (splitCounts level first distance s).lab s.hits first (s.cellend[first]! + 1 - first)

Count splitting orders the whole cell by its hit values. Only the initial key must lie below the second-minimum sentinel.