Checked finite separator solution

The selected theorem is obtained from the finite suffix-state completion in MarshallHall.Separation. The implementation's separator is repackaged at the Challenge boundary so the Comparator sees the explicit finite action, not only its finite-index stabilizer corollary.

structure LERFChallenge.FinitePermutationSeparator {α : Type u} (H : Subgroup (FreeGroup α)) (g : FreeGroup α) : Type (u + 1)

A finite permutation action with a base state fixed by the subgroup and moved by the separating element.

• State : Type u

  The finite set of states on which the free group acts.

• stateFintype : Fintype self.State

  A finite enumeration of the action states.

• representation : FreeGroup α →* Equiv.Perm self.State

  The homomorphism realizing the free group as permutations of the state set.

• base : self.State

  The distinguished state fixed by the subgroup and moved by the separating element.

• fixes_subgroup (h : ↥H) : (self.representation ↑h) self.base = self.base
• separates : (self.representation g) self.base ≠ self.base

theorem LERFChallenge.freeGroup_finite_permutation_separator {α : Type u_1} (H : Subgroup (FreeGroup α)) [Group.FG ↥H] (g : FreeGroup α) (hg : g ∉ H) : Nonempty (FinitePermutationSeparator H g)