Proposição 3.14: alternating normal form for $3$ -braids

Proved

TarchaBraids.prop_3_14_three_braid_alternating_form

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

algebraic-topologybraid-groupsfundamental-groupgroup-theory

Tarcha's Proposição 3.14 states that every braid on three strands can be written in the alternating form

\sigma_1^{a_1}\sigma_2^{b_1}\sigma_1^{a_2}\sigma_2^{b_2}\cdots\sigma_1^{a_m}\sigma_2^{b_m},

where the exponents $a_2,\dots,a_m$ and $b_1,\dots,b_{m-1}$ are non-zero, while the first exponent $a_1$ and the last exponent $b_m$ are allowed to vanish. The normalization is exactly what one obtains by grouping a word in $\sigma_1^{\pm1},\sigma_2^{\pm1}$ into maximal alternating blocks: a vanishing interior exponent would allow two neighbouring blocks to be merged.

The formal statement quantifies over finite sequences of exponent pairs $(a_j, b_j)$ , requires the product of the corresponding blocks to equal the given braid, and imposes the non-vanishing conditions on all pairs except the first component of the first pair and the second component of the last pair. The empty sequence is permitted and represents the identity braid.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinBraidGroup

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem prop_3_14_three_braid_alternating_form (b : ArtinBraidGroup 3) :
    ∃ l : List (ℤ × ℤ),
      b = (l.map (fun p =>
            sigma (0 : Fin (3 - 1)) ^ p.1 * sigma (1 : Fin (3 - 1)) ^ p.2)).prod ∧
      (∀ p ∈ l.tail, p.1 ≠ 0) ∧ (∀ p ∈ l.dropLast, p.2 ≠ 0) := 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.14, pp. 56–57

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 $3$ strands: the group presented by two generators, indexed by $\{0, 1\}$ , subject to Artin's relators, which for this index set consist of the single braid relation between the two consecutive indices (no pair of indices is at distance at least $2$ ). Write $\sigma_1$ and $\sigma_2$ for the images of the generators with index $0$ and $1$ .

Let $b$ be an arbitrary element of this group. The claim is that there exists a finite list

L = \bigl[(a_1,b_1), (a_2,b_2), \dots, (a_m,b_m)\bigr]

of pairs of integers, possibly the empty list, such that all three of the following hold.

$b$ equals the product, in the order of the list, of the elements $\sigma_1^{a_j}\sigma_2^{b_j}$ , i.e.

b = \sigma_1^{a_1}\sigma_2^{b_1}\,\sigma_1^{a_2}\sigma_2^{b_2}\cdots\sigma_1^{a_m}\sigma_2^{b_m},

with integer exponents that may be negative or zero; the empty list gives the identity element. 2. Every pair after the first one has non-zero first component: $a_j \neq 0$ for $2 \le j \le m$ . 3. Every pair before the last one has non-zero second component: $b_j \neq 0$ for $1 \le j \le m-1$ .

Nothing is required of $a_1$ or of $b_m$ , and no uniqueness or minimality of the list is asserted. For a list of length $0$ or $1$ conditions 2 and 3 are vacuous.

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.14: alternating normal form for 333-braids

Proposição 3.14: alternating normal form for $3$ -braids