theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.orbit {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel tv last : Nat} {f : Frame n} {leaf : State n} {parents : Parents n} {base : List (Fin n)} {gs : List (Perm n)} (h : FirstInput G tcLevel f parents) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (htv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv) (horbit : (cheapCheck true f.level (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.snd.snd).orbits[tv]! = tv) (path : have p := Frame.firstParent G.graph tcLevel f [] tv; have ch := Parent.child G.graph tcLevel p; Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel ch.level ch.numcells ch.entry last leaf) (hf : n ≤ f.level + fuel) (hbase : ∀ (b : Fin n), f.entry.fixedpts.mem ↑b = true ↔ b ∈ base) (htrace : Generation.Realizes G gs (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel (fuel + 1) f.level f.numcells f.entry).snd.genTrace.toList) : have guide := ⟨tv, ⋯⟩; ∀ (v : Fin n), Aut.Orbit G.toDense base guide v → Generation.Carries G.toDense gs base guide v

The actual guiding child and its complete sibling suffix generate the guide's whole point-stabilizer orbit. The stored reference, its orbit transport, and every suffix invariant are derived from the first descent.