theorem Hex.GraphIso.Nauty.Sparse.splitCounts_constant {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) (key : Nat → Nat) (hl : s.lab.size = n) (hs : s.ptn.size = n) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (hv : ∀ (v : Nat), v ∈ segN s.lab first (s.cellend[first]! + 1 - first) → s.hits[v]! = key v) (a len : Nat) (ho : IsCell (splitCounts level first distance s).ptn level a len) (ha : first ≤ a) (he : a + len ≤ s.cellend[first]! + 1) (q r : Nat) : a ≤ q → q < a + len → a ≤ r → r < a + len → key (splitCounts level first distance s).lab[q]! = key (splitCounts level first distance s).lab[r]!

Each fragment produced by the executed splitter has a constant semantic key whenever the incoming hit array represents that key on the split cell. Only those vertices need a count interpretation; other scratch is unrestricted.