theorem Hex.GraphIso.Nauty.Max.firstPath_cover {n k : Nat} {G : Colored n k} {tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hp : Generic.FirstPath { g := rowsOf G } tcLevel fuel level numcells st last leaf) (hn : ∀ (q : Nat), q < fuel → (contract G tcLevel).nodeValid q (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel q)) {cs bs fs : List Nat} {parents : Parents n} (hi : NodeInput G { g := rowsOf G } tcLevel fuel true { level := level, numcells := numcells, codes := cs, entry := st } bs fs parents) {base : List (Fin n)} {gs : List (Perm n)} (hbase : ∀ (b : Fin n), st.fixedpts.mem ↑b = true ↔ b ∈ base) (htrace : Generation.Realizes G gs (node true { g := rowsOf G } (n + 2) tcLevel fuel level numcells st).snd.genTrace.toList) (hopen : (Generic.prepareFirst { g := rowsOf G } tcLevel level numcells st).fst ≠ n) : ∃ (guide : Fin n), ↑guide = ((Generic.prepareFirst { g := rowsOf G } tcLevel level numcells st).snd.snd.fst.nextElem none).getD 0 ∧ ∀ (v : Fin n), Aut.Orbit G base guide v → Generation.Carries G gs base guide v

An internal actual first node covers the full orbit of its guiding vertex in any final containing trace. Guiding return, reference transport, and every suffix input are constructed from the node's actual path.