theorem Hex.GraphIso.Aut.raw_mem {n k : Nat} {G : Colored n k} {γ : Array Nat} (h : γ ∈ raw G) : ∃ (p : Perm n), p ∈ gens G ∧ ∀ (i : Fin n), ↑(p.get i) = γ[↑i]!

Each checked raw array represents an element of the returned list.

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

theorem Hex.GraphIso.Aut.generated_word {n k : Nat} {G : Colored n k} (w : List (Array Nat)) : (∀ (γ : Array Nat), γ ∈ w → γ ∈ raw G) → ∃ (p : Perm n), Perm.Generated (gens G) p ∧ ∀ (v : Fin n), ↑(p.get v) = Nauty.applyWord w ↑v

A forward word in the checked raw arrays is a generated permutation, with the same action on every vertex.

theorem Hex.GraphIso.Aut.generated_of_wordConn {n k : Nat} {G : Colored n k} {u v : Fin n} (h : Nauty.WordConn (raw G) ↑u ↑v) : ∃ (p : Perm n), Perm.Generated (gens G) p ∧ p.get u = v

The search's word connectivity supplies subgroup membership, not just an arbitrary automorphism carrying the vertex.

theorem Hex.GraphIso.Aut.generated_orbits {n k : Nat} (G : Colored n k) (v : Fin n) : ∃ (p : Perm n), Perm.Generated (gens G) p ∧ ↑(p.get v) = (orbits G)[↑v]!

The recorded representative is reached inside the generated subgroup.

theorem Hex.GraphIso.Aut.generated_of_orbits_eq {n k : Nat} {G : Colored n k} {u v : Fin n} (h : (orbits G)[↑u]! = (orbits G)[↑v]!) : ∃ (p : Perm n), Perm.Generated (gens G) p ∧ p.get u = v

Equal recorded representatives give an element of the generated subgroup carrying one vertex to the other.

theorem Hex.GraphIso.Aut.gens_mem {n k : Nat} {G : Colored n k} {p : Perm n} (h : p ∈ gens G) : ∃ (γ : Array Nat), γ ∈ raw G ∧ ∀ (i : Fin n), ↑(p.get i) = γ[↑i]!

Every returned generator has its corresponding checked raw array.

theorem Hex.GraphIso.Aut.orbits_flat {n k : Nat} (G : Colored n k) : Nauty.Orbit.Flat (orbits G) n

theorem Hex.GraphIso.Aut.orbits_raw {n k : Nat} {G : Colored n k} {γ : Array Nat} (hγ : γ ∈ raw G) {i : Nat} (hi : i < n) : (orbits G)[γ[i]!]! = (orbits G)[i]!

Every generator edge has equal recorded representatives.

theorem Hex.GraphIso.Aut.orbits_generated {n k : Nat} {G : Colored n k} {p : Perm n} (h : Perm.Generated (gens G) p) (v : Fin n) : (orbits G)[↑(p.get v)]! = (orbits G)[↑v]!

Recorded representatives are invariant under the entire generated subgroup.

theorem Hex.GraphIso.Aut.generated_iff_orbits_eq {n k : Nat} {G : Colored n k} {u v : Fin n} : (∃ (p : Perm n), Perm.Generated (gens G) p ∧ p.get u = v) ↔ (orbits G)[↑u]! = (orbits G)[↑v]!

The orbit array is exactly the orbit partition of the generated subgroup.