theorem Hex.GraphIso.Nauty.Max.root_generates {n k : Nat} (G : Colored n k) (hn0 : 0 < n) (hn : ∀ (f : Nat), f < n + 2 → (contract G 100).nodeValid f (Generic.nodeCall { g := rowsOf G } (n + 2) 100 f)) {p : Perm n} (hp : IsIso G G p) : Perm.Generated (List.filterMap (autom? G) (runColoredTraced G).autos.toList) p

The actual nonempty root generates every graph automorphism from its own emitted trace, assuming only strictly smaller maximum contracts.

theorem Hex.GraphIso.Nauty.Max.zero_generates {k : Nat} (G : Colored 0 k) (p : Perm 0) : Perm.Generated (List.filterMap (autom? G) (runColoredTraced G).autos.toList) p

The empty graph's automorphism is generated by the empty word.