theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.suffix {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel tv last : Nat} {f : Frame n} {leaf : State n} {parents : Parents 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) : have l := { node := f, first := true }; have c := Loop.cell G.graph tcLevel l; have p := Frame.firstParent G.graph tcLevel f [] tv; have back := Parent.firstBack G.graph tcLevel fuel p; ∃ (bs : List Nat), ∃ (fs : List Nat), SweepInput G tcLevel l bs fs (p.cell.nextElem (some tv)) p.cell back parents ∧ back.eqlevFirst = f.level ∧ f.level < back.allsamelevel ∧ Generic.sweep true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (n + 1) f.level c.numcells p.tc tv (some tv) p.cell 0 p.state = Generic.sweep true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel n f.level c.numcells p.tc tv (p.cell.nextElem (some tv)) p.cell (if (back.orbits[tv]! == tv) = true then 1 else 0) back

The actual guiding child establishes the complete suffix context, its boundary values and the literal continuation equation. These are derived from the executed child's maximum and normal-return theorems, without any generation or orbit-count premise.