theorem Hex.GraphIso.Nauty.Sparse.splitCounts_control {n : 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 : ∀ (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) (hc : CountTrace.control s = CountTrace.control t) (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)))) : CountTrace.control (splitCounts level first distance s) = CountTrace.control (splitCounts level first distance t)

Equal cell count multisets and initial control yield literally equal hashes, active sets and ordered queues in the executed splitter. Scratch storage and vertex order may differ.

theorem Hex.GraphIso.Nauty.Sparse.splitCounts_equiv {n : Nat} (σ : Renaming n) (level first last : Nat) (distance : Bool) (s t : RefineSt n) (hsl : s.lab.toList.Perm (List.range n)) (htl : t.lab.toList.Perm (List.range 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) (hk : ∀ (v : Nat), v ∈ segN s.lab first (last + 1 - first) → t.hits[σ.toFun v]! = s.hits[v]!) (hc : IsCell s.ptn level first (last + 1 - first)) (hp : cellsPerm s.ptn level t.lab (Array.map σ.toFun s.lab)) (hcontrol : CountTrace.control s = CountTrace.control t) (hnum : s.numcells = t.numcells) : (splitCounts level first distance s).ptn = (splitCounts level first distance t).ptn ∧ cellsPerm (splitCounts level first distance s).ptn level (splitCounts level first distance t).lab (Array.map σ.toFun (splitCounts level first distance s).lab) ∧ CountTrace.control (splitCounts level first distance s) = CountTrace.control (splitCounts level first distance t) ∧ (splitCounts level first distance s).numcells = (splitCounts level first distance t).numcells

All count-split observations commute with renaming and within-cell permutation: ordered partition, cell contents, control and exact count. Only the divided cell's hit values must agree under the renaming.