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

Every generator array emitted by the initialized sparse search is a colour-preserving automorphism. All histories, references and allocation premises are derived from initialization, including the empty graph.

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

Final row installation retains the sound trace literally.

theorem Hex.GraphIso.Nauty.Sparse.generator_iso {n k : Nat} (G : Sparse.Colored n k) {values : Array Nat} (h : values ∈ (runColored G).genTrace) : ∃ (p : Perm n), Sparse.IsIso G G p ∧ values.size = n ∧ ∀ (v : Fin n), values[↑v]! = ↑(p.get v)

Each literal emitted array has the graph's order and is exactly the forward map of a native colour-preserving automorphism. This soundness theorem does not yet assert that the trace generates the entire group.