Tarcha 3.15 outer and outside-strand coordinate facts
ProvedTarchaBraids.thm_3_15_adjacent_outer_outside_facts_v1artin-presentationbraid-groupsgeometrytarcha
The outer-rotation comparison path has the three stated local coordinates, and all nonlocal strands are fixed by the left word, right word and outer rotation.
Preamble
import Mathlib import Definitions.Def_TarchaBraids_adjacent_geometry_interfaces_v1
Formal statement
namespace TarchaBraids
open BraidsLinksMCG
theorem thm_3_15_adjacent_outer_outside_facts_v1 :
∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
AdjacentOuterOutsideFacts i j hji := by sorry
end TarchaBraidsSource
Modular local-coordinate and fixed-outside-strand extraction from the explicit adjacent Artin relation proof.