Tarcha 3.15 left piecewise braid path equals the three-half-twist word
ProvedTarchaBraids.thm_3_15_left_word_identification_v1artin-presentationbraid-groupspath-concatenationtarcha
The projected piecewise left adjacent braid path is exactly the concatenation of the three half-twist loops i, j, i.
Preamble
import Mathlib import Definitions.Def_TarchaBraids_adjacent_config_data_v1 import Definitions.Def_TarchaBraids_adjacent_word_loops_v1
Formal statement
namespace TarchaBraids
open BraidsLinksMCG
theorem thm_3_15_left_word_identification_v1 :
∀ {n : ℕ} (i j : Fin (n - 1)) (q : unitInterval),
configProj n (leftBraidConfig n i j (q : ℝ)) = leftBraidWordLoop n i j q := by sorry
end TarchaBraidsSource
Modular path-identification layer extracted from Tarcha's adjacent Artin relation proof.