theorem Hex.GraphIso.Nauty.Sparse.runState_pairs {n k : Nat} (G : Sparse.Colored n k) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; PairsOk G (runState (Graph.ofGraph G.graph) p.fst p.snd).snd

Every pair retained by the actual initialized sparse search has checked root-colour-preserving realizers. The proof covers explicit and implicit admissions, full workspace replacement and the empty graph.

theorem Hex.GraphIso.Nauty.Sparse.runColored_pairs {n k : Nat} (G : Sparse.Colored n k) : PairsOk G (runColored G)

Final native row installation preserves the validated bounded pruning workspace literally; it adds no checks or replay to execution.