Tarcha right adjacent interpolation as an ordered configuration
DefinitionTarchaBraids_right_interp_config_data_v1artin-presentationbraid-groupsconfiguration-spacetarcha
The collision-free right interpolation between the adjacent three-half-twist word and the common outer-rotation path, packaged as an ordered configuration using the accepted injectivity theorem.
Definition code
import Mathlib
import Definitions.Def_TarchaBraids_adjacent_path_data_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_right_interp_injective_v1
namespace TarchaBraids
noncomputable section
open BraidsLinksMCG
def rightOuterInterpConfig {n : ℕ} (i j : Fin (n - 1))
(hji : (j : ℕ) = (i : ℕ) + 1) (u q : unitInterval) : OrderedConfig n :=
⟨rightOuterInterpFun n i j (u : ℝ) (q : ℝ),
thm_3_15_adjacent_right_interp_injective_v1
i j hji (u : ℝ) (q : ℝ) u.2.1 u.2.2 q.2.1 q.2.2⟩
end
end TarchaBraids
Source
Modular ordered-configuration layer for Tarcha's explicit adjacent Artin relation proof.