theorem Hex.GraphIso.Nauty.Sparse.firstPath_codes {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel numcells last : Nat} {st leaf : State n} (hn : 0 < n) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel 1 numcells st last leaf) (h : NodeInv G 1 numcells st) (htsize : n < st.firsttc.size) (hfsize : st.firstcode.size = n + 2) (hcsize : st.canoncode.size = n + 2) : ∃ (codes : List Nat), codes.length = last ∧ Codes codes codes (firstterminal last leaf) ∧ FirstCodeInv n codes codes (firstterminal last leaf).firstcode (firstterminal last leaf).eqlevFirst

The literal first leaf initializes both comparison machines with the codes executed along its native descent. Their storage and code bounds are derived from the descent, rather than assumed at the leaf.

theorem Hex.GraphIso.Nauty.Sparse.initial_codes {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) : have p := initialPartitionWith n k G.coloring.cells.toArray Fin.val; ∃ (last : Nat), ∃ (leaf : State n), ∃ (codes : List Nat), ∃ (l : Label n), Generic.FirstPath (Graph.ofGraph G.graph) 100 (n + 2) 1 p.snd.length (initial (Graph.ofGraph G.graph) p.fst p.snd) last leaf ∧ codes.length = last ∧ codes ≠ [] ∧ Label.ofArray? n leaf.lab = some l ∧ Codes codes codes (firstterminal last leaf) ∧ FirstCodeInv n codes codes (firstterminal last leaf).firstcode (firstterminal last leaf).eqlevFirst ∧ State.best G.graph (firstterminal last leaf) = some { codes := codes ++ [codeSentinel], graph := G.graph.relabel l.perm }

Initialization supplies an actual first leaf and both initialized comparison machines. The readable incumbent is that leaf's sparse key.