Tarcha 3.15: adjacent half-twists satisfy the braid relation

Proved

TarchaBraids.thm_3_15_half_twists_adjacent_braid_v1

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

artin-presentationbraid-groupshalf-twisttarcha

For the standard geometric half-twist generators of the n-strand braid group, adjacent generators satisfy the three-term braid relation. This is the local three-strand isotopy used in the Artin presentation.

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_adjacent_braid_v1 (n : ℕ) :
    ∀ 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

Source-faithful child of TarchaBraids.thm_3_15_half_twists_satisfy_relations, corresponding to the adjacent braid relation in Tarcha's Teorema 3.15.

View graph