theorem Hex.GraphIso.Nauty.Sparse.firstPath_canonical {n k : Nat} {G : Sparse.Colored n k} (hn : 0 < n) {tcLevel fuel level numcells last : Nat} {st leaf : State n} (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf) (hl : 1 ≤ level) (h : NodeInv G level numcells st) : CanonLabel G (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

The first leaf installs a valid incumbent, and all ancestor sweeps retain its validity throughout the actual remaining production search.

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

The nonempty production root returns an installed, colour-respecting canonical label. The initializer supplies all first-descent premises.