theorem Hex.GraphIso.Nauty.Generation.FirstTail.cover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {inf tcLevel specFuel runFuel level numcells tc len tv1 e boundary oRef : Nat} {codes fs targets : List Nat} {rsLab rsPtn : Array Nat} {entry : SearchSt n} {key : Key n} {base : List (Fin n)} {guide : Fin n} (hg : ctx.g = rowsOf G) (hinf : inf = n + 2) (hpath : level = codes.length) (hrun : n + 2 < level + 1 + runFuel) (hboundary : level < boundary) (href : oRef < len) (hp : ChildPath ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc targets key oRef) (hmove : ∀ (v : Fin n), Aut.Orbit G base guide v → ∀ (o : Nat), o < len → rsLab[tc + o]! = ↑v → ChildPath ctx tcLevel boundary level (LoopInv.frame rsLab rsPtn numcells) tc targets key o) (hfixFrame : ∀ (γ : Array Nat), CellStab rsPtn level rsLab γ → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) {loopFuel : Nat} {cursor : Option Nat} {tcell : VSet n} {st : SearchSt n} {best : Option (Key n)} {trail : FrameTrail} (sweep : FirstTail G ctx inf tcLevel specFuel runFuel level numcells tc len tv1 e codes fs rsLab rsPtn entry loopFuel cursor tcell st best trail) (hm : Matches ctx (level + 1) st targets key) (heq : st.eqlevFirst = level) (hsame : boundary ≤ st.allsamelevel) (hfuel : n < cursorRank cursor + loopFuel) (hfirst : st.firstlab[tc]! = ↑guide) (hpast : CanonPast level tc cursor st) (hcover : Cover G base guide tcell cursor) (index : Nat) (htrace : ∀ (γ : Array Nat), γ ∈ (firstChildLoop ctx inf tcLevel runFuel loopFuel level numcells tc tv1 (tcell.nextElem cursor) tcell index st).snd.snd.genTrace → γ ∈ Aut.trace G) (v : Fin n) : Aut.Orbit G base guide v → Aut.Carries G base guide v

The first-path tail covers the entire true orbit of its guiding child by words in the final emitted generators. Reference transport uses the true path stabilizer; only recorded return carriers require generation.