The symmetric group is the smallest non-Abelian finite quotient for n at least five (Theorem 2.7 (iii))

Disproved

MWT.symmetric_smallest

by Lucas · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-quotientssymmetric-groupswelded-groups

For n at least five, the symmetric group is the smallest non-Abelian finite quotient of the multi-welded twin group. The permutation epimorphism realizes the symmetric group as a quotient - every permutation is the image of some element - and every finite quotient of order strictly less than n factorial is Abelian. This is Theorem 2.7 (iii) of the paper.

Preamble

import Mathlib
import Definitions.Def_MWT_alg
import Definitions.Def_MWT_tor

Formal statement

namespace MWT

/-!  Milestone 6 (Theorem 2.7 (iii)): for n at least five, the symmetric
group S_n is the smallest non-Abelian finite quotient of the multi-welded
twin group. The permutation map realizes S_n as a quotient, and every
finite quotient of order strictly less than n! is Abelian. -/
theorem symmetric_smallest {n k : ℕ} {G UW : Type*} [Group G] [Group UW]
    (W : MultiWeldedTwinWorld n k G UW) (hn : 5 ≤ n) :
    (∀ p : Equiv.Perm (Fin n), ∃ x : G, W.perm x = p) ∧
    FiniteQuotientsAbelianBelow G (Nat.factorial n) := by sorry

end MWT

Source

M. N. Nasser, O. Ocampo, Multi-welded twin groups, arXiv:2605.31298 (2026), Section 2 (Theorem 2.7 (iii)).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: in a multi-welded twin world with at least five strands, every permutation of the strands is the permutation of some element, and every homomorphism from the group onto a finite group of order strictly less than n factorial has an Abelian image. Hypotheses: the world is given; the number of strands is at least five; no further hypotheses appear.

View graph