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

Disproved

MWT.finite_quotient_witness

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

finite-quotientssymmetric-groupswelded-groups

The multi-welded twin group admits a marked finite quotient of order at least 2^k n!: a homomorphism to the product of the symmetric group with an elementary Abelian 2-group A of order 2^(k+1), whose first component is the permutation map, and whose second component separates the twin generator from each virtual generator - the image of the product of the twin generator and the virtual generator of any family is a nontrivial element of A. This is the witnessing construction of Theorem 2.7 (iv) of the paper.

Preamble

import Mathlib
import Definitions.Def_MWT_alg
import Definitions.Def_MWT_tor

Formal statement

namespace MWT

/-!  Milestone 7 (Theorem 2.7 (iv), construction): the multi-welded twin
group admits a marked finite quotient of order at least 2^k n!: a
homomorphism to the product of the symmetric group with an elementary
Abelian 2-group A of order 2^(k+1), whose first component is the
permutation map, and whose second component separates the twin generator
from each virtual generator - the images of s_i and rho_i^(alpha) differ
in A. -/
theorem finite_quotient_witness {n k : ℕ} {G UW : Type*} [Group G] [Group UW]
    (W : MultiWeldedTwinWorld n k G UW) :
    ∃ (A : Type) (_ : CommGroup A) (_ : Fintype A) (hA : Fintype.card A = 2 ^ (k + 1))
      (th : G →* Equiv.Perm (Fin n) × A),
      (∀ x : G, (th x).1 = W.perm x) ∧
      (∀ (i : Fin (n - 1)) (α : Fin k), (th (W.s i * W.rho α i)).2 ≠ 1) := 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 witnessing construction).

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 Abelian group A of order 2^(k+1) and a homomorphism from the group to the product of the symmetric group with A, such that the first component of the image of any element is its permutation, and the second component of the image of the product of any twin generator with the virtual generator of the same position of any family is not the identity. Hypotheses: the world is given; no further hypotheses appear.

View graph