theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.index {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel tv last : Nat} {f : Frame n} {leaf : State n} {parents : Parents n} {base : List (Fin n)} [DecidableRel (Aut.Orbit G.toDense base)] (h : FirstInput G tcLevel f parents) (hi : (visit (Graph.ofGraph G.graph) f.level f.numcells f.entry).fst < n) (htv : (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv) (horbit : (cheapCheck true f.level (Generic.prepareFirst (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry).snd.snd.snd.snd).orbits[tv]! = tv) (path : have p := Frame.firstParent G.graph tcLevel f [] tv; have ch := Parent.child G.graph tcLevel p; Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel ch.level ch.numcells ch.entry last leaf) (hf : n ≤ f.level + fuel) (hbase : ∀ (b : Fin n), f.entry.fixedpts.mem ↑b = true ↔ b ∈ base) (hreplay : OrbitReplay f.entry) : have guide := ⟨tv, ⋯⟩; have l := { node := f, first := true }; have c := Loop.cell G.graph tcLevel l; have p := Frame.firstParent G.graph tcLevel f [] tv; (Generic.sweep true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (n + 1) f.level c.numcells p.tc tv (some tv) p.cell 0 p.state).snd.fst = List.countP (fun (v : Fin n) => decide (Aut.Orbit G.toDense base guide v)) (List.finRange n)

The actual first sweep returns the exact size of the guide's full point-stabilizer orbit. The first child initializes the count, and every later mark is justified at the state where the executable reads it.