theorem Hex.GraphIso.Nauty.Sparse.splitCounts_keys {n q : Nat} (level first last : Nat) (distance : Bool) (s t : RefineSt n) (hsl : s.lab.size = n) (htl : t.lab.size = n) (hse : s.cellend[first]! = last) (hte : t.cellend[first]! = last) (hf : first ≤ last) (hb : last < n) (hsk : s.hits[s.lab[first]!]! < n + 2) (htk : t.hits[t.lab[first]!]! < n + 2) (hp : (List.map (fun (v : Nat) => s.hits[v]!) (segN s.lab first (last + 1 - first))).Perm (List.map (fun (v : Nat) => t.hits[v]!) (segN t.lab first (last + 1 - first)))) (hq : first ≤ q) (he : q ≤ last) : s.hits[(splitCounts level first distance s).lab[q]!]! = t.hits[(splitCounts level first distance t).lab[q]!]!

Equal input count multisets yield identical ordered output counts in the actual splitter. Other scratch fields need not agree.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_ptn {n : Nat} (level first last : Nat) (distance : Bool) (s t : RefineSt n) (hsl : s.lab.size = n) (htl : t.lab.size = n) (hsp : s.ptn.size = n) (htp : t.ptn = s.ptn) (hse : s.cellend[first]! = last) (hte : t.cellend[first]! = last) (hf : first ≤ last) (hb : last < n) (hsk : ∀ (q : Nat), first ≤ q → q ≤ last → s.hits[s.lab[q]!]! < n + 2) (htk : ∀ (q : Nat), first ≤ q → q ≤ last → t.hits[t.lab[q]!]! < n + 2) (hp : (List.map (fun (v : Nat) => s.hits[v]!) (segN s.lab first (last + 1 - first))).Perm (List.map (fun (v : Nat) => t.hits[v]!) (segN t.lab first (last + 1 - first)))) : (splitCounts level first distance s).ptn = (splitCounts level first distance t).ptn

Count splitting writes the same partition for equal cell key multisets. This is literal array equality, including inherited boundary values.