theorem Hex.GraphIso.Nauty.Sparse.refineWith_cert {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) (hinv : CertInv (Graph.context G) level { lab := lab, ptn := ptn, active := active, numcells := numcells, hint := 0, maxpos := 0, longcode := numcells }) : CertInv (Graph.context G) level (refineWith (Graph.ofGraph G) level lab ptn active numcells scratch).toPartition

The complete executed refinement preserves the equitability certificate, including the distance branch, both splitter passes, and queue selection.