theorem Hex.GraphIso.Nauty.Sparse.cellStab_refineWith {n : Nat} (G : SparseGraph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) (hp : lab.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 scratch) {gamma : Array Nat} (hg : checkAutom (Graph.context G).g gamma = true) (hc : CellStab ptn level lab gamma) : have r := refineWith (Graph.ofGraph G) level lab ptn active numcells scratch; CellStab r.ptn level r.lab gamma

A checked automorphism stabilizing the input cells also stabilizes the cells produced by the actual cached sparse refinement. The proof uses native refinement equivariance with the same input on both sides.