theorem Hex.GraphIso.Nauty.Sparse.firstPath_stabilizes {n k : Nat} {G : Sparse.Colored n k} {base cells : Nat} {root : State n} (hp : Ready G base cells root) (hn : 0 < n) (hb : 1 ≤ base) {tcLevel fuel level numcells last : Nat} {st leaf : State n} (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel level numcells st last leaf) (hlevel : base < level) (hi : NodeInv G level numcells st) (hframe : FrameOut G base base root st) (hwork : st.workperm.size = n) (htrace : st.genTrace = #[]) : TraceFrame G base root (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel level numcells st).snd

A successful actual first descent initializes the frozen ancestor's reference and generator invariant, then preserves it through every later child and return. Only the incoming empty trace and workspace allocation are assumed; reference containment is derived from the installed first leaf.