Every geometric braid loop has a finite signed half-twist normal form

Open

TarchaBraids.every_loop_homotopic_braidWord_v1

by WillR · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-topologybraid-groupsconfiguration-spacegenerationtarcha

Every based loop in the unordered configuration space of n points in the plane is path-homotopic, relative to its endpoints, to a finite concatenation of elementary adjacent half-twist loops and their reverses. This is the path-level normal-form statement underlying Tarcha's proof that the Artin half-twists generate the geometric braid group.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_TarchaBraids_HalfTwist
import Definitions.Def_TarchaBraids_generation_word_data_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem every_loop_homotopic_braidWord_v1 (n : ℕ) :
    EveryLoopHasBraidWord n := by sorry

end TarchaBraids

Source

Tarcha Teorema 3.11, pp. 55-56: subdivide a braid by finitely many level planes so that each slab contains one crossing and is equivalent to an Artin generator or its inverse.

View graph