Tarcha 3.15 left adjacent braid local coordinate facts
ProvedTarchaBraids.thm_3_15_adjacent_left_local_facts_v1artin-presentationbraid-groupsgeometrytarcha
The explicit left adjacent three-half-twist word satisfies all nine phase-by-phase coordinate formulas on its three distinguished local strands.
Preamble
import Mathlib import Definitions.Def_TarchaBraids_adjacent_geometry_interfaces_v1
Formal statement
namespace TarchaBraids
open BraidsLinksMCG
theorem thm_3_15_adjacent_left_local_facts_v1 :
∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
AdjacentLeftLocalFacts i j hji := by sorry
end TarchaBraidsSource
Modular local-coordinate extraction from the explicit adjacent Artin relation proof.