theorem Hex.GraphIso.Nauty.Sparse.CountSort.firstRun_uniform (lab hits : Array Nat) (first last : Nat) (hf : first < last) (hk : ∀ (q : Nat), first ≤ q → q < last → hits[lab[q]!]! = hits[lab[first]!]!) : firstRun lab hits first last = last

A constant-count cell exhausts the initial equal-count scan.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_uniform {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (hf : first ≤ s.cellend[first]!) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! = s.hits[s.lab[first]!]!) : splitCounts level first distance s = s.hash first

A uniform count cell returns immediately after hashing its start. No scratch array, partition, counter, or active-queue entry changes.