Proposição 3.13: every $2$ -braid is a power of $\sigma_1$

Proved

TarchaBraids.prop_3_13_two_braid_is_power

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

algebraic-topologybraid-groupsfundamental-groupgroup-theory

Tarcha's Proposição 3.13 states that every braid on two strands is $\sigma_1^m$ for some integer $m$ . Here $B_2$ is the abstract braid group on two strands, presented by the single generator $\sigma_1$ with no relations (there are no pairs of indices at distance $\ge 2$ and no consecutive pairs available), so the claim is that

\forall\, b \in B_2,\ \exists\, m \in \mathbb{Z},\quad b = \sigma_1^{\,m},

the exponent $m$ being allowed to be negative or zero. Together with $\sigma_1$ having infinite order this identifies $B_2$ with $\mathbb{Z}$ , but only the displayed statement is asserted.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem prop_3_13_two_braid_is_power (b : ArtinBraidGroup 2) :
    ∃ m : ℤ, b = sigma (0 : Fin (2 - 1)) ^ m := 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.13, p. 56

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.

The statement concerns the abstract braid group on $2$ strands: the group presented by generators indexed by $\{0\}$ (one generator, since $2 - 1 = 1$ ) subject to Artin's relators, of which there are none for this index set — the commutation relators require two indices at distance at least $2$ and the braid relators require two consecutive indices, and neither exists in a one-element index set. Write $\sigma$ for the image of the single generator.

The claim: for every element $b$ of this group there exists an integer $m$ , possibly negative or zero, with

b = \sigma^{\,m},

the power being the integer power in the group. No uniqueness of $m$ is asserted, and no claim is made that $\sigma$ has infinite order.

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.13: every 222-braid is a power of σ1\sigma_1σ1​

Proposição 3.13: every $2$ -braid is a power of $\sigma_1$