theorem Hex.GraphIso.Nauty.Sparse.runColored_generates {n k : Nat} (G : Sparse.Colored n k) {p : Perm n} (hp : Sparse.IsIso G G p) : Perm.Generated (runColored G).generators p

The complete generator trace of the executed sparse search generates every colour-preserving automorphism, including at order zero. No second search or assumed recursive correctness contract is used.

theorem Hex.GraphIso.Nauty.Sparse.generated_iff {n k : Nat} (G : Sparse.Colored n k) (p : Perm n) : Perm.Generated (runColored G).generators p ↔ Sparse.IsIso G G p

Membership in the subgroup generated by the actual sparse output is equivalent to being an automorphism of the native ordered-colour graph.