theorem Hex.GraphIso.Nauty.Generation.first_generates {n k : Nat} (G : Colored n k) (tcLevel fuel level numcells : Nat) (codes : List Nat) (st : SearchSt n) (trail : FrameTrail) (base : List (Fin n)) : FirstInv G { g := rowsOf G } level codes numcells st trail → PathOk { g := rowsOf G } (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st → st.noncheaplevel ≤ level → CheapDesc { g := rowsOf G } level st.noncheaplevel (refine { g := rowsOf G } level st.lab st.ptn st.active numcells) → OrbSound (OrbConn st.genTrace.toList n) st.orbits n → 1 ≤ level → level = codes.length + 1 → st.firsttc.size = n + 2 → n + 2 < level + fuel → (∀ (b : Fin n), st.fixedpts.mem ↑b = true ↔ b ∈ base) → (∀ (γ : Array Nat), γ ∈ (firstPathNode { g := rowsOf G } (n + 2) tcLevel fuel level numcells st).snd.genTrace → γ ∈ Aut.trace G) → ∀ (p : Perm n), IsIso G G p → Perm.Fixes base p → Perm.Generated (Aut.gens G) p

The first-path stabilizer induction. Every automorphism fixing the individualized base is generated by the final public list, provided the actual node's trace is included in that list's raw trace.