theorem Hex.GraphIso.Aut.complete {n k : Nat} (G : Colored n k) {p : Perm n} (hp : IsIso G G p) : Perm.Generated (gens G) p

The discovered generators generate every automorphism of the graph.

theorem Hex.GraphIso.autos_complete {n k : Nat} (G : Colored n k) {p : Perm n} (hp : IsIso G G p) : Perm.Generated (autos G).gens p

Completeness: every automorphism is a word in the returned generators.

theorem Hex.GraphIso.Aut.orbits_eq_iff_sameOrbit {n k : Nat} (G : Colored n k) (u v : Fin n) : (orbits G)[↑u]! = (orbits G)[↑v]! ↔ SameOrbit G u v

The orbit array is exactly the orbit partition of the full automorphism group.

theorem Hex.GraphIso.autos_sameOrbit {n k : Nat} (G : Colored n k) (u v : Fin n) : (autos G).orbits[↑u]! = (autos G).orbits[↑v]! ↔ SameOrbit G u v

Two vertices have the same returned representative exactly when an automorphism carries one onto the other.