A finite quotient of order at least 2^k n! exists (Theorem 2.7 (iv))

Proved

MWT.finite_quotient_order

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

finite-quotientsgroup-orderswelded-groups

The multi-welded twin group admits a finite quotient whose order is at least 2^k n!, which is strictly larger than the order of the symmetric group whenever k is at least one. The quotient is the image of the marked homomorphism into the product of the symmetric group with the elementary Abelian 2-group of rank k+1: the image contains the whole symmetric factor and, for each family, a distinct nontrivial element of the 2-group. This is Theorem 2.7 (iv) of the paper, the main structural lower bound.

Preamble

import Mathlib
import Definitions.Def_MWT_alg
import Definitions.Def_MWT_tor

Formal statement

namespace MWT

/-!  The goal (Theorem 2.7 (iv)): the multi-welded twin group M_kWT_n
admits a finite quotient whose order is at least 2^k n!, strictly larger
than the order of the symmetric group for k at least one. The quotient is
the image of the marked homomorphism of Milestone 7 into the product of the
symmetric group with the elementary Abelian 2-group of rank k+1. -/
theorem finite_quotient_order {n k : ℕ} {G UW : Type*} [Group G] [Group UW]
    (W : MultiWeldedTwinWorld n k G UW) :
    ∃ (F : Type) (_ : Group F) (_ : Fintype F) (q : G →* F),
      2 ^ k * Nat.factorial n ≤ Fintype.card F := by sorry

end MWT

Source

M. N. Nasser, O. Ocampo, Multi-welded twin groups, arXiv:2605.31298 (2026), Section 2 (Theorem 2.7 (iv), the main structural lower bound).

Read-back

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

Restate: in a multi-welded twin world, there exist a finite group F and a homomorphism from the group onto F such that the order of F is at least the product of 2^k with the factorial of the number of strands. Hypotheses: the world is given; no further hypotheses appear.

View graph