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

The actual sparse production root always returns a valid installed canonical prefix. Its initial blank allocation and first leaf supply every premise, including the zero-colour empty graph.

theorem Hex.GraphIso.Nauty.Sparse.runColored_store {n k : Nat} (G : Sparse.Colored n k) : Store G.graph (runColored G)

Finishing fills the remaining rows without changing the checked label.

theorem Hex.GraphIso.Nauty.Sparse.canong_prefix {n k : Nat} (G : Sparse.Colored n k) : (runColored G).canong.Prefix (G.graph.relabel (Sparse.label G).perm) n

The complete raw canonical store represents the native public label's relabelling. Raw row order is retained; normalized row equality is semantic.

theorem Hex.GraphIso.Nauty.Sparse.canong_canon {n k : Nat} (G : Sparse.Colored n k) : (runColored G).canong.Prefix (Sparse.canon G).graph n

theorem Hex.GraphIso.Nauty.Sparse.canong_rows {n k : Nat} (G : Sparse.Colored n k) (i : Fin n) : (SparseGraph.row (runColored G).canong.offsets (runColored G).canong.neighbors ↑i).toList.Perm (List.map Fin.val ((Sparse.canon G).graph.nbrs i).toList)

Each returned working row has exactly the public canonical graph's neighbours, including the executable's retained neighbour order.