theorem Hex.GraphIso.Nauty.Sparse.firstPath_returned {n k : Nat} {G : Sparse.Colored n k} (hn : 0 < n) {tcLevel fuel level numcells last : Nat} {st leaf : State n} {fs : List Nat} (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf) (hl : 1 ≤ level) (hi : NodeInv G level numcells st) (hshape : FirstShape G.graph level numcells st) (htsize : n < st.firsttc.size) (hcsize : n + 1 < st.firstcode.size) (hblank : st.canong.toRows = (Graph.ofGraph G.graph).blank) (hwork : st.workperm.size = n) (htrace : TraceOk G st) (hfuel : n + 1 ≤ level + fuel) (hflen : fs.length = last) (hterminal : Comparison G.graph fs fs fs (firstterminal last leaf)) : ∃ (bs : List Nat), ReturnCodes G.graph (List.take (level - 1) fs) bs fs (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

The actual first descent supplies settled comparisons to every ancestor's later siblings. The leaf comparison is initialized separately from its recorded native codes; recovery reads their exact ancestor prefix.