theorem Hex.GraphIso.Nauty.Sparse.runState_reference {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; have out := (runState (Graph.ofGraph G.graph) p.fst p.snd).snd; ∃ (last : Nat), ∃ (leaf : State n), 1 ≤ last ∧ last ≤ n ∧ Ready G last n leaf ∧ SearchState.reference out = (firstterminal last leaf).reference ∧ Depth last out

The completed nonempty root saves its actual first leaf, whose depth bounds every subsequent first-code comparison. The sentinel and reference come from execution, with all premises derived from initialization.

theorem Hex.GraphIso.Nauty.Sparse.firstlab_size {n k : Nat} (G : Sparse.Colored n k) : (runColored G).firstlab.size = n

theorem Hex.GraphIso.Nauty.Sparse.firstlab_cellsReach {n k : Nat} (G : Sparse.Colored n k) : CellsReach G.toDense (runColored G).firstlab

The saved first label, as well as the final incumbent, respects every original colour cell. It is suitable for a checked automorphism scatter.

theorem Hex.GraphIso.Nauty.Sparse.firstlab_perm {n k : Nat} (G : Sparse.Colored n k) : (runColored G).firstlab.toList.Perm (List.range n)