theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_equiv {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) (level split : Nat) (s t : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hq : t.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (he : t.ptn = s.ptn) (hend : s.ptn[n - 1]! ≤ level) (hsp : split < n) (hc : IsCell s.ptn level split 1) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) (hj : Index.Valid n t.lab t.ptn level t.cellstart t.cellend) (hperm : cellsPerm s.ptn level t.lab (Array.map (renamingOf p).toFun s.lab)) (hm : Scratch.Marks n s.stamp s.marks) (hv : Scratch.Marks n s.stamp s.vmarks) (hn : Scratch.Marks n t.stamp t.marks) (hw : Scratch.Marks n t.stamp t.vmarks) (hcontrol : CountTrace.control s = CountTrace.control t) (hnum : s.numcells = t.numcells) : have a := splitSingleton (Graph.ofGraph G) level split s; have b := splitSingleton (Graph.ofGraph H) level split t; a.ptn = b.ptn ∧ cellsPerm a.ptn level b.lab (Array.map (renamingOf p).toFun a.lab) ∧ CountTrace.control a = CountTrace.control b ∧ a.numcells = b.numcells

The full executed singleton pass commutes with graph renaming and permutations within input cells. Hashes, ordered queues, active sets, partition entries and cell counts agree literally. The two valid caches, mark generations and native row orders may differ.