theorem Hex.GraphIso.Nauty.Sparse.refineWith_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 : Nat) (lab out ptn : Array Nat) (active : VSet n) (numcells : Nat) (s t : Scratch) (hp : lab.toList.Perm (List.range n)) (hq : out.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (ha : ∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) (hb : Scratch.Bounded n s) (hc : Scratch.Bounded n t) (hcell : cellsPerm ptn level out (Array.map (renamingOf p).toFun lab)) : RefineSt.Equiv (renamingOf p) level (refineWith (Graph.ofGraph G) level lab ptn active numcells s) (refineWith (Graph.ofGraph H) level out ptn active numcells t)

Full production refinement commutes with graph renaming and arbitrary orders within input cells. All partition and control observations agree, independently of bounded incoming scratch, stale hits and cache generations. The proof includes empty queues, index rebuilding, shallow native distance splitting, both main-loop branches and final hash cleanup.