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]!]!)
:
A uniform count cell returns immediately after hashing its start. No scratch array, partition, counter, or active-queue entry changes.