theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.generated_visit {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel boundary tv : Nat} {l : Loop n} {bs fs : List Nat} {cell : VSet n} {st out : State n} {parents : Parents n} {targets : List Nat} {key : Key n} {previous : Option Nat} {short : Bool} {gs : List (Perm n)} {base : List (Fin n)} {guide : Fin n} (h : SweepInput G tcLevel l bs fs (some tv) cell st parents) (hf : l.first = true) (hbudget : n ≤ l.node.level + fuel) (hm : Generation.Matches G.graph (l.node.level + 1) st targets key) (heq : st.eqlevFirst = l.node.level) (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 = some tv → Generation.CanonPast l.node.level c.tc previous st → Generation.Cover G.toDense gs base guide cell previous → st.firstlab[c.tc]! = ↑guide → Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (l.node.level + 1) (c.numcells + 1) (Generic.Policy.child l.first l.node.level c.tc tv st) = (Generic.Exit.unwind l.node.level short, out) → Generation.Realizes G gs out.genTrace.toList → Generation.Cover G.toDense gs base guide cell (some tv)

A visited first-path sibling advances generated coverage of the guide's true stabilizer orbit. Matching reference completion is proved for the actual cached child; every carrier comes from its emitted trace.