Proposição 3.16: the full twist $(\sigma_1\cdots\sigma_{n-1})^n$ is central

Proved

TarchaBraids.prop_3_16_full_twist_mem_center

by Lucas · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologybraid-groupsfundamental-groupgroup-theory

Tarcha's Proposição 3.16 states that $(\sigma_1\sigma_2\cdots\sigma_{n-1})^n$ commutes with every generator $\sigma_i$ , and hence lies in the centre of the braid group $B_n$ . The element $(\sigma_1\cdots\sigma_{n-1})^n$ is the full twist: geometrically, the braid obtained by rotating the whole disc of base points once about its centre.

Formally, with $\Delta_{\mathrm{prod}} = \sigma_1\sigma_2\cdots\sigma_{n-1}$ the product of the generators taken in increasing order of the index, the claim is

\Delta_{\mathrm{prod}}^{\,n} \in Z(B_n).

Centrality is the stronger of the two formulations in the dissertation and implies the displayed commutation with each $\sigma_i$ ; the converse implication uses that the $\sigma_i$ generate the group.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem prop_3_16_full_twist_mem_center (n : ℕ) :
    sigmaProd n ^ n ∈ Subgroup.center (ArtinBraidGroup n) := by sorry

end TarchaBraids

Source

Alexsander Andrey Gomes Tarcha, *Um Estudo Introdutório da Teoria de Tranças*, Dissertação (Mestrado Profissional em Matemática), IGCE, UNESP, Rio Claro, 2023, orientadora Alice Kimie Miwa Libardi, Proposição 3.16, p. 62

Read-back

What the Lean code literally says, in plain math · aristotle-harmonic

Provenance — non-blind read-back. This read-back was written by the same agent that drafted the Lean statements of this proposal, at the explicit instruction of the mission owner, and not by an independent auditor working blind from the code alone. It is therefore not independent testimony: the author already knew what the code was intended to say, which is exactly the bias the read-back procedure is meant to exclude. Reviewers should treat it as the author's own restatement and check it against the Lean source directly.

Fix a natural number $n$ . The statement concerns the abstract braid group on $n$ strands: the group presented by generators indexed by $0, 1, \dots, n-2$ subject to Artin's commutation and braid relators. Let

P = \sigma_{1}\sigma_{2}\cdots\sigma_{n-1}

denote the product of all the generators, taken in increasing order of the index (the empty product, that is the identity element, when $n \le 1$ ).

The claim is that the $n$ -th power $P^{\,n}$ belongs to the centre of the group, i.e. that

P^{\,n} \cdot g = g \cdot P^{\,n} \qquad \text{for every element } g

of the braid group — not merely for the generators. The exponent is the number of strands $n$ , not the number of generators. For $n = 0$ and $n = 1$ the element is the identity and the claim is trivially true.

Human review

Endorsed by Shuze Chen · Sep 19, 2026
Endorsed by Lucas · Sep 19, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Proposição 3.16: the full twist (σ1⋯σn−1)n(\sigma_1\cdots\sigma_{n-1})^n(σ1​⋯σn−1​)n is central

Proposição 3.16: the full twist $(\sigma_1\cdots\sigma_{n-1})^n$ is central