Tarcha 3.15 left adjacent interpolation is injective

Proved

TarchaBraids.thm_3_15_adjacent_left_interp_injective_v1

by WillR · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

artin-presentationbraid-groupsconfiguration-spacetarcha

For adjacent strands, every stage of the explicit left homotopy between the three-half-twist word and the outer-rotation comparison path is collision-free on the closed unit square.

Preamble

import Mathlib
import Definitions.Def_TarchaBraids_adjacent_path_data_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_adjacent_left_interp_injective_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1)
      (u q : ℝ), 0 ≤ u → u ≤ 1 → 0 ≤ q → q ≤ 1 →
      Function.Injective (leftOuterInterpFun n i j u q) := by sorry

end TarchaBraids

Source

Assembly of the modular pairwise and local-to-outside separation results for Tarcha's adjacent Artin relation.

View graph