A signed half-twist word evaluates to its concatenated geometric loop

Proved

TarchaBraids.braidWord_free_eval_v1

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

braid-groupsfree-groupsfundamental-groupgenerationtarcha

For every finite signed word in the adjacent Artin generators, evaluating the word in the free group and then sending each generator to the corresponding elementary half-twist gives exactly the fundamental-group class of the concatenated positive and negative half-twist loops. The path concatenation order follows the pinned convention for the fundamental group multiplication.

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 braidWord_free_eval_v1 :
    ∀ {n : ℕ} (w : List (BraidLetter n)),
      FreeGroup.lift (fun i : Fin (n - 1) => halfTwistBraid n i) (braidWordFree w) =
        FundamentalGroup.fromPath
          (Path.Homotopic.Quotient.mk (braidWordLoop n w)) := by sorry

end TarchaBraids

Source

Algebraic/path bookkeeping for Tarcha Teorema 3.11, using the signed braid-word data and the pinned reversed path-concatenation convention.

View graph