theorem
Hex.GraphIso.Nauty.Max.SweepInput.generated_tail
{n k : Nat}
{G : Colored n k}
{tcLevel fuel cfuel boundary level numcells tc tv1 index : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : Search n}
{l : Loop n}
{bs fs : List Nat}
{parents : Parents n}
(h : SweepInput G { g := rowsOf G } tcLevel fuel cfuel true level numcells tc tv1 cursor cell index st l bs fs parents)
(hn : ∀ (q : Nat), q ≤ fuel → (contract G tcLevel).nodeValid q (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel q))
(hpast : Generic.Past true tv1 cursor)
{R : RefineSt n}
{targets : List Nat}
{key : Key n}
(hit : IterOk { g := rowsOf G } level R)
(hlab : R.lab = (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.snd.lab)
(hptn : R.ptn = (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.snd.ptn)
(hnc : R.numcells = numcells)
(hleaf :
Generation.HasLeaf { g := rowsOf G } tcLevel level R (tc :: targets)
{ codes := R.longcode :: key.codes, rows := key.rows })
(hm :
Generation.Matches { g := rowsOf G } level st (tc :: targets) { codes := R.longcode :: key.codes, rows := key.rows })
(hg : st.gcaFirst = level)
(heq : st.eqlevFirst = level)
(hboundary : level < boundary)
(hsame : boundary ≤ st.allsamelevel)
{gs : List (Perm n)}
{base : List (Fin n)}
{guide : Fin n}
(hmove :
∀ (v : Fin n),
Aut.Orbit G base guide v →
∀ (o : Nat),
o < (Loop.prepare { g := rowsOf G } tcLevel l).snd.snd.snd.fst →
R.lab[tc + o]! = ↑v → Generation.ChildPath { g := rowsOf G } tcLevel boundary level R tc targets key o)
(hfixFrame : ∀ (γ : Array Nat), CellStab R.ptn level R.lab γ → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b)
{previous : Option Nat}
(hnext : cell.nextElem previous = cursor)
(hcanon : Generation.CanonPast level tc previous st)
(hcover : Generation.Cover G gs base guide cell previous)
(hfirst : st.firstlab[tc]! = ↑guide)
(htrace :
Generation.Realizes G gs
(sweep true { g := rowsOf G } (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index
st).snd.snd.genTrace.toList)
(v : Fin n)
:
Aut.Orbit G base guide v → Generation.Carries G gs base guide v
The actual first-path sibling suffix covers the guide's full orbit by generators in any final containing trace. Every received reference is proved by the smaller node call, and every skip uses a recorded word.