theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.generated_tail {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel cfuel boundary tv1 index : Nat} {l : Loop n} {bs fs : List Nat} {cursor previous : Option Nat} {cell : VSet n} {st : State n} {parents : Parents n} {targets : List Nat} {key : Key n} {gs : List (Perm n)} {base : List (Fin n)} {guide : Fin n} (h : SweepInput G tcLevel l bs fs cursor cell st parents) (hf : l.first = true) (hbudget : n ≤ l.node.level + fuel) (hcursor : Generic.CursorFuel n cfuel cursor) (hpast : Generic.Past l.first tv1 cursor) (hm : Generation.Matches G.graph (l.node.level + 1) st targets key) (heq : st.eqlevFirst = l.node.level) (hboundary : l.node.level < boundary) (hsame : boundary ≤ st.allsamelevel) : have c := Loop.cell G.graph tcLevel l; have R := State.refined (Graph.ofGraph G.graph) l.node.level l.node.numcells l.node.entry; (∀ (v : Fin n), Aut.Orbit G.toDense base guide v → ∀ (o : Nat), o < c.len → R.lab[c.tc + o]! = ↑v → Generation.ChildPath G.graph tcLevel boundary l.node.level R c.tc targets key o) → (∀ (gamma : Array Nat), CellStab R.ptn l.node.level R.lab gamma → ∀ (b : Fin n), b ∈ base → gamma[↑b]! = ↑b) → cell.nextElem previous = cursor → Generation.CanonPast l.node.level c.tc previous st → Generation.Cover G.toDense gs base guide cell previous → st.firstlab[c.tc]! = ↑guide → Generation.Realizes G gs (Generic.sweep l.first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel l.node.level c.numcells c.tc tv1 cursor cell index st).snd.snd.genTrace.toList → ∀ (v : Fin n), Aut.Orbit G.toDense base guide v → Generation.Carries G.toDense gs base guide v

The complete native first-path sibling suffix covers the guide's true stabilizer orbit in any group containing its emitted generators. Actual child returns supply reference carriers; orbit skips use words in the recorded trace, and the proof follows every literal cursor advance.