Tarcha 3.15 right piecewise braid path equals the three-half-twist word
ProvedTarchaBraids.thm_3_15_right_word_identification_v1artin-presentationbraid-groupspath-concatenationtarcha
The projected piecewise right adjacent braid path is exactly the concatenation of the three half-twist loops j, i, j.
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_right_word_identification_v1 :
∀ {n : ℕ} (i j : Fin (n - 1)) (q : unitInterval),
configProj n (rightBraidConfig n i j (q : ℝ)) = rightBraidWordLoop n i j q := by sorry
end TarchaBraidsSource
Modular path-identification layer extracted from Tarcha's adjacent Artin relation proof.