theorem Hex.GraphIso.Nauty.Sparse.Max.FirstInput.generates {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel last : Nat} {f : Frame n} {leaf : State n} {parents : Parents n} {base : List (Fin n)} {gs : List (Perm n)} (h : FirstInput G tcLevel f parents) (path : Generic.FirstPath (Graph.ofGraph G.graph) tcLevel fuel f.level f.numcells f.entry last leaf) (hf : n + 1 ≤ f.level + fuel) (hbase : ∀ (b : Fin n), f.entry.fixedpts.mem ↑b = true ↔ b ∈ base) (htrace : Generation.Realizes G gs (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).snd.genTrace.toList) (p : Perm n) : Sparse.IsIso G G p → Perm.Fixes base p → Perm.Generated gs p

Every sparse automorphism fixing the actual individualized base is generated by the first call's emitted trace. The induction uses the executed guiding child and its proved complete stabilizer-orbit coverage.