Teorema 3.15 (homomorphism step): the half-twists satisfy Artin's relations

Proved

TarchaBraids.thm_3_15_half_twists_satisfy_relations

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

algebraic-topologybraid-groupsfundamental-groupgroup-theory

The first half of the proof of Tarcha's Teorema 3.15 checks that the assignment $x_i \mapsto [\sigma_i]$ respects the defining relations, so that it extends to a group homomorphism from the abstractly presented group to the braid group. Geometrically this is exactly the pair of relations of Proposição 3.14 and of the discussion following it, verified for the half-twist loops themselves:

[\mathrm{ht}_i]\,[\mathrm{ht}_j] = [\mathrm{ht}_j]\,[\mathrm{ht}_i] \qquad (|i-j| \ge 2),

[\mathrm{ht}_i]\,[\mathrm{ht}_{i+1}]\,[\mathrm{ht}_i] = [\mathrm{ht}_{i+1}]\,[\mathrm{ht}_i]\,[\mathrm{ht}_{i+1}].

The first relation holds because half-twists with non-adjacent indices are supported in disjoint discs; the second is the braid relation, whose proof in the dissertation is the isotopy displayed in Figura 3.17 and its generalization.

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_15_half_twists_satisfy_relations (n : ℕ) :
    (∀ i j : Fin (n - 1), 2 ≤ ((i : ℤ) - (j : ℤ)).natAbs →
        halfTwistBraid n i * halfTwistBraid n j = halfTwistBraid n j * halfTwistBraid n i) ∧
    (∀ i j : Fin (n - 1), (j : ℕ) = (i : ℕ) + 1 →
        halfTwistBraid n i * halfTwistBraid n j * halfTwistBraid n i =
          halfTwistBraid n j * halfTwistBraid n i * halfTwistBraid n j) := 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 e comentários seguintes, pp. 56–57 (relação de trança e relação de comutação), usados na demonstração do Teorema 3.15, pp. 57–58

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 $0, 1, \dots, n-2$ (an empty range when $n \le 1$ ). For each index $i$ , $\mathrm{ht}_i$ denotes the class, in the fundamental group of the unordered configuration space of $n$ points of the plane based at the class of $(1,2,\dots,n)$ , of the loop rotating the points $i+1$ and $i+2$ counterclockwise by $\pi$ about their midpoint while all other points remain fixed.

The statement is a conjunction of two universally quantified claims about products in that group.

For all indices $i$ and $j$ in the range, if the absolute value of the difference of the two indices, computed in the integers, is at least $2$ , then

\mathrm{ht}_i \cdot \mathrm{ht}_j = \mathrm{ht}_j \cdot \mathrm{ht}_i .

For all indices $i$ and $j$ in the range, if the value of $j$ is exactly the value of $i$ plus one, then

\mathrm{ht}_i \cdot \mathrm{ht}_j \cdot \mathrm{ht}_i = \mathrm{ht}_j \cdot \mathrm{ht}_i \cdot \mathrm{ht}_j .

Both conditions are hypotheses on the indices only; the products are taken in the fundamental group with its usual (concatenation-induced) multiplication. When $n \le 2$ the index conditions cannot be met in the second clause, and when $n \le 1$ both clauses 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