Marshall Hall's theorem through finite cores

The finite-core completion developed in MarshallHall.Hall proves the inclusion-compatible free-factor form of Marshall Hall's theorem. The same repository also contains the LERF consequence, the binary and finite-indexed free-group Grushko rank calculations, and the factorwise infrastructure for the arbitrary-factor theorem.

Arbitrary-factor Grushko--Neumann

theorem MarshallHall.rank_freeProduct_eq_add {G H : Type u} [Group G] [Group H] [Group.FG G] [Group.FG H] : Group.rank (Monoid.Coprod G H) = Group.rank G + Group.rank H

The rank of a free product of two finitely generated groups is additive.

The proof is the finite labelled-graph reduction: a minimal null path yields either a safe fold or, after source-unfolding, a safe fold followed by an explicit monochromatic-vertex contraction. The resulting strict decrease in the finite graph supplies the strong induction on the number of vertices.

Public LERF surfaces. The explicit permutation separator is the primary finite-quotient formulation; the stabilizer formulation is its existential finite-index corollary.

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

theorem freeGroup_subgroup_separable {α : Type u_1} (H : Subgroup (FreeGroup α)) [Group.FG ↥H] (g : FreeGroup α) (hg : g ∉ H) : ∃ (K : Subgroup (FreeGroup α)), H ≤ K ∧ K.index ≠ 0 ∧ g ∉ K