Teorema 3.11: the half-twists generate $\pi_1(B_{0,n}E^2)$

Open

TarchaBraids.thm_3_11_half_twists_generate

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

algebraic-topologybraid-groupsfundamental-groupgroup-theory

Tarcha's Teorema 3.11 states that every $n$ -braid can be written as a product of the Artin generators $\sigma_1^{\pm 1}, \dots, \sigma_{n-1}^{\pm 1}$ . In the configuration-space model an $n$ -braid is a class in $\pi_1(B_{0,n}E^2, *)$ and the Artin generator $\sigma_{i+1}$ is the class of the elementary half-twist that interchanges the base points $i+1$ and $i+2$ .

The assertion is therefore that the subgroup generated by the $n-1$ half-twist classes is the whole fundamental group:

\bigl\langle\, [\mathrm{ht}_0], [\mathrm{ht}_1], \dots, [\mathrm{ht}_{n-2}] \,\bigr\rangle = \pi_1\bigl(B_{0,n}E^2, *\bigr).

Since a subgroup is closed under inverses, writing a braid as a word in the generators and their inverses is the same as saying it lies in this subgroup. For $n \le 1$ there are no generators and the statement asserts that the fundamental group is trivial.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_TarchaBraids_HalfTwist

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_11_half_twists_generate (n : ℕ) :
    Subgroup.closure (Set.range (fun i : Fin (n - 1) => halfTwistBraid n i)) =
      (⊤ : Subgroup (GeomBraidGroup 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, Teorema 3.11, p. 55 (demonstração pp. 55–56, Figuras 3.14–3.16)

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$ . Generator indices run over the $n-1$ values $0, 1, \dots, n-2$ (with truncated subtraction, so for $n = 0$ and $n = 1$ this index set is empty). For each such index $i$ the statement refers to a fixed element $\mathrm{ht}_i$ of the fundamental group of the unordered configuration space of $n$ points of the plane, based at the class of $(1,2,\dots,n)$ : the class of the loop that rotates the two points $i+1$ and $i+2$ counterclockwise by $\pi$ about their midpoint while the other points stay fixed.

The claim is an equality of subgroups of that fundamental group: the subgroup generated by the set $\{\mathrm{ht}_i : 0 \le i \le n-2\}$ — the smallest subgroup containing all of them, hence containing all finite products of these elements and their inverses — equals the whole group.

For $n = 0$ and $n = 1$ the generating set is empty and the claim says that the fundamental group of the configuration space in question is the trivial group.

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

Teorema 3.11: the half-twists generate π1(B0,nE2)\pi_1(B_{0,n}E^2)π1​(B0,n​E2)

Teorema 3.11: the half-twists generate $\pi_1(B_{0,n}E^2)$