theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.index_tail {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel cfuel boundary index : Nat} {l : Loop n} {bs fs : List Nat} {cursor previous : Option Nat} {cell : VSet n} {st : State n} {parents : Parents n} {targets : List Nat} {key : Key n} {base : List (Fin n)} {guide : Fin n} [DecidablePred (Aut.Orbit G.toDense base guide)] (h : SweepInput G tcLevel l bs fs cursor cell st parents) (hf : l.first = true) (hbudget : n ≤ l.node.level + fuel) (hcursor : Generic.CursorFuel n cfuel cursor) (hpast : Generic.Past l.first (↑guide) cursor) (hm : Generation.Matches G.graph (l.node.level + 1) st targets key) (heq : st.eqlevFirst = l.node.level) (hboundary : l.node.level < boundary) (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) → (∀ (v : Fin n), Aut.Orbit G.toDense base guide v → cell.mem ↑v = true) → (∀ (v : Fin n), Aut.Orbit G.toDense base guide v → ↑guide ≤ ↑v) → cell.nextElem previous = cursor → Generation.CanonPast l.node.level c.tc previous st → Generation.Cover G.toDense st.generators base guide cell previous → st.firstlab[c.tc]! = ↑guide → OrbitReplay st → Generation.Counter (Aut.Orbit G.toDense base guide) previous index → (Generic.sweep l.first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel l.node.level c.numcells c.tc (↑guide) cursor cell index st).snd.fst = List.countP (fun (v : Fin n) => decide (Aut.Orbit G.toDense base guide v)) (List.finRange n)

The executed sibling suffix counts every vertex of the guide's true stabilizer orbit exactly once. Coverage uses the generators emitted at each counter update, rather than generators discovered afterwards.