Tarcha 3.15 left interpolation local-to-outside separation
ProvedTarchaBraids.thm_3_15_adjacent_left_outside_separation_v1artin-presentationbraid-groupsconfiguration-spacetarcha
Throughout the explicit left interpolation, each distinguished local strand remains distinct from every nonlocal strand.
Preamble
import Mathlib import Definitions.Def_TarchaBraids_adjacent_separation_interfaces_v1
Formal statement
namespace TarchaBraids
open BraidsLinksMCG
theorem thm_3_15_adjacent_left_outside_separation_v1 :
∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
AdjacentLeftOutsideSeparationFacts i j hji := by sorry
end TarchaBraidsSource
Modular local-to-outside separation layer of the explicit adjacent Artin relation interpolation proof.