theorem Hex.GraphIso.Nauty.Sparse.splitNontrivial_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 len : 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) (hc : IsCell s.ptn level split len) (hb : split + len ≤ n) (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) (hh : s.hits.size = n) (hn : Scratch.Marks n t.stamp t.marks) (hk : t.hits.size = n) (hcontrol : CountTrace.control s = CountTrace.control t) (hnum : s.numcells = t.numcells) : have a := splitNontrivial (Graph.ofGraph G) level split s; have b := splitNontrivial (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 complete executed nontrivial pass commutes with graph renaming and permutations within input cells. All scalar and control observations agree literally, with independently allocated caches and retained scratch.