theorem Hex.GraphIso.Nauty.Sparse.refineWith_congr {n : Nat} (G : SparseGraph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (s t : 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 s) (hc : Scratch.Bounded n t) : have a := refineWith (Graph.ofGraph G) level lab ptn active numcells s; have b := refineWith (Graph.ofGraph G) level lab ptn active numcells t; a.lab = b.lab ∧ a.ptn = b.ptn ∧ a.active = b.active ∧ a.queue = b.queue ∧ a.numcells = b.numcells ∧ a.longcode = b.longcode

Reusing any bounded scratch gives the same literal refinement result: labels, partition, active set, ordered queue, cell count and hash all agree. The retained scratch arrays and generations themselves need not coincide. This follows the executed index rebuild, shallow BFS branch, singleton and count splitters, main loop and final cleanup.