theorem Hex.PermGroup.Partition.invariant_spec {n : ℕ} (p : Partition n) (G : Group n) : p.IsInvariant G ↔ ∀ g ∈ closure G.generators, ∀ (x y : Fin n), p.toSetoid x y ↔ p.toSetoid (g x) (g y)

Computational block invariance agrees with preservation by every permutation in the Mathlib subgroup generated by the original input.

theorem Hex.PermGroup.Group.blocks_spec {n : ℕ} (G : Group n) (pairs : List (Fin n × Fin n)) : IsLeast {r : Setoid (Fin n) | (∀ g ∈ closure G.generators, ∀ (x y : Fin n), r x y → r (g x) (g y)) ∧ ∀ q ∈ pairs, r q.1 q.2} (G.blocks pairs).toSetoid

The result is the least invariant Mathlib equivalence relation containing the seeds. This includes its admissibility, not merely a one-sided bound.

theorem Hex.PermGroup.Group.blocks_sInf {n : ℕ} (G : Group n) (pairs : List (Fin n × Fin n)) : (G.blocks pairs).toSetoid = sInf {r : Setoid (Fin n) | (∀ g ∈ closure G.generators, ∀ (x y : Fin n), r x y → r (g x) (g y)) ∧ ∀ q ∈ pairs, r q.1 q.2}

Minimality identifies the executable result with the infimum of all admissible equivalence relations in Mathlib's complete lattice.

theorem Hex.PermGroup.BlockAction.mem_ker {n : ℕ} {G : Group n} {p : Partition n} {hp : p.IsInvariant G} (a : BlockAction G p hp) (g : Element G) : g ∈ a.image.hom.ker ↔ ∀ (x : Fin n), p.toSetoid ((↑g).toEquiv x) x

The homomorphism kernel fixes every block setwise, retaining the original degree and allowing nontrivial permutations inside each block.

theorem Hex.PermGroup.BlockAction.order_mul_image {n : ℕ} {G : Group n} {p : Partition n} {hp : p.IsInvariant G} (a : BlockAction G p hp) : G.order = a.kernel.group.order * a.image.group.order