Documentation

HexGraphIso.Nauty.Sparse.CountUniform

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.