theorem Hex.GraphIso.Nauty.Sparse.splitCounts_lab {n : Nat} (level first : Nat) (distance : Bool) (s t : RefineSt n) (hl : t.lab = s.lab) (he : t.cellend[first]! = s.cellend[first]!) (hf : first ≤ s.cellend[first]!) (hb : s.cellend[first]! < s.lab.size) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! = t.hits[s.lab[q]!]!) : (splitCounts level first distance s).lab = (splitCounts level first distance t).lab

Equal input labels and observed cell counts give literally equal output labels in the executed count splitter. All other scratch entries and the unrelated partition, queue and hash fields may differ.