theorem
Hex.GraphIso.Nauty.Sparse.Max.FirstInput.order
{n k : ℕ}
{G : Sparse.Colored n k}
{tcLevel fuel last : ℕ}
{f : Frame n}
{leaf : State n}
{parents : Parents n}
{base : List (Fin 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)
(hreplay : OrbitReplay f.entry)
:
(Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel f.level f.numcells f.entry).2.order = f.entry.order * Nat.card ↥(Sparse.Aut.stabilizer G base)
The literal accumulator of a first-path call multiplies its incoming value by the order of the full automorphism stabilizer of its actual base.