Tarcha 3.15 adjacent braid words have the common q=1 endpoint

Proved

TarchaBraids.thm_3_15_adjacent_word_one_endpoints_v1

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

artin-presentationbraid-groupsendpointstarcha

For adjacent strands, both explicit three-half-twist coordinate words end at the same ordered configuration, obtained from the base configuration by swapping the two outer local strands.

Preamble

import Mathlib
import Definitions.Def_TarchaBraids_adjacent_path_data_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_adjacent_word_one_endpoints_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)), (j : ℕ) = (i : ℕ) + 1 →
      leftBraidFun n i j 1 =
        (baseOrdered n).1 ∘ Equiv.swap (strandIdx i) (strandIdxSucc j) ∧
      rightBraidFun n i j 1 =
        (baseOrdered n).1 ∘ Equiv.swap (strandIdx i) (strandIdxSucc j) := by sorry

end TarchaBraids

Source

Modular q=1 endpoint extraction from the explicit adjacent Artin relation proof.

View graph