theorem Hex.GraphIso.Nauty.Sparse.firstPath_history {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells last : Nat} {st leaf : State n} (hn : 0 < n) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf) (hl : 1 ≤ level) (h : NodeInv G level numcells st) (htsize : n < st.firsttc.size) (hcsize : n < st.firstcode.size) : ∃ (xs : List (Nat × Nat)), ∃ (U : RefineSt n), ∃ (codes : List Nat), ∃ (trace : CodePath G.graph level (State.refined (Graph.ofGraph G.graph) level numcells st) xs last U codes), CodePath.Selects tcLevel trace ∧ Targets leaf.firsttc level (List.map Prod.fst xs) ∧ StoredCodes leaf.firstcode level codes ∧ U.lab = leaf.lab ∧ U.ptn = leaf.ptn ∧ discreteAt U.ptn last n = true

The actual first descent stores its selected native target path and every executed refinement code. Its mathematical leaf has the literal label and partition of the prepared production leaf.