theorem Hex.GraphIso.Nauty.Generation.FirstHead.cover {n k : Nat} {G : Colored n k} {tcLevel specFuel runFuel level numcells tc len e : Nat} {codes : List Nat} {rsLab rsPtn : Array Nat} {tcell : VSet n} {pre : SearchSt n} {trail : FrameTrail} {base : List (Fin n)} {guide : Fin n} (hpath : level = codes.length) (hrun : n + 2 < level + 1 + runFuel) (htcsize : pre.firsttc.size = n + 2) (hwindow : tcell = windowSet n rsLab tc len) (hbase : ∀ (b : Fin n), pre.fixedpts.mem ↑b = true ↔ b ∈ base) (hdeep : ∀ (p : Perm n), IsIso G G p → Perm.Fixes (guide :: base) p → Perm.Generated (Aut.gens G) p) (head : FirstHead G { g := rowsOf G } (n + 2) tcLevel specFuel runFuel level numcells tc len (↑guide) e codes rsLab rsPtn tcell pre trail) (htrace : ∀ (γ : Array Nat), γ ∈ (firstChildLoop { g := rowsOf G } (n + 2) tcLevel runFuel (n + 1) level numcells tc (↑guide) (tcell.nextElem none) tcell 0 pre).snd.snd.genTrace → γ ∈ Aut.trace G) (v : Fin n) : Aut.Orbit G base guide v → Aut.Carries G base guide v

A complete first-path sweep generates the full orbit of its guiding vertex, assuming generation in the next point stabilizer. The guiding short-prune filter and all later visits use the actual search trace.