theorem Hex.GraphIso.Aut.indiv_of_orbitSize {n k : ℕ} {G : Colored n k} (v : Fin n) (h : 1 < orbitSize G v) : ∃ (H : Colored n (k + 1)), indiv? G v = some H

A non-singleton orbit supplies another vertex in the selected colour cell, so the checked individualization succeeds.

def Hex.GraphIso.Aut.indivEquiv {n k : ℕ} {G : Colored n k} {v : Fin n} {H : Colored n (k + 1)} (h : indiv? G v = some H) : ↥(MulAction.stabilizer (↥(group G)) v) ≃ ↥(group H)

The individualized graph's full automorphism group is the point stabilizer in the original full group.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Aut.indiv_card {n k : ℕ} {G : Colored n k} {v : Fin n} {H : Colored n (k + 1)} (h : indiv? G v = some H) : Nat.card ↥(group G) = orbitSize G v * Nat.card ↥(group H)

Orbit-stabilizer for the exact individualization used by orderAux.

theorem Hex.GraphIso.Aut.orderAux_card {n : ℕ} (fuel : ℕ) {k : ℕ} (G : Colored n k) : n ≤ k + fuel → orderAux fuel G (orbits G) = Nat.card ↥(group G)

One unit of fuel per remaining possible colour suffices for the existing orbit-stabilizer recursion. No additional search bookkeeping is needed: every successful recursive step adds a colour.

theorem Hex.GraphIso.Aut.order_card {n k : ℕ} (G : Colored n k) : order G = Nat.card ↥(group G)

The reported order is the cardinality of the full colour-preserving automorphism group.