Tarcha 3.15 left interpolation pairwise local separation
ProvedTarchaBraids.thm_3_15_adjacent_left_pairwise_separation_v1artin-presentationbraid-groupsconfiguration-spacetarcha
Throughout the explicit left interpolation, the three distinguished local strands remain pairwise distinct for all interpolation and path parameters in the unit interval.
Preamble
import Mathlib import Definitions.Def_TarchaBraids_adjacent_separation_interfaces_v1
Formal statement
namespace TarchaBraids
open BraidsLinksMCG
theorem thm_3_15_adjacent_left_pairwise_separation_v1 :
∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
AdjacentLeftPairwiseSeparationFacts i j hji := by sorry
end TarchaBraidsSource
Modular pairwise-separation layer of the explicit adjacent Artin relation interpolation proof.