Prove2Me

Tarcha 3.15 left interpolation ordered configuration is continuous

Proved
TarchaBraids.thm_3_15_left_interp_config_continuous_v1

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

artin-presentationbraid-groupscontinuitytarcha

The collision-free left interpolation between the adjacent braid word and the common outer rotation is continuous as a two-parameter map into ordered configuration space.

Preamble
import Mathlib
import Definitions.Def_TarchaBraids_left_interp_config_data_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_raw_continuous_v1
Formal statement
namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_left_interp_config_continuous_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
      Continuous (fun z : unitInterval × unitInterval =>
        leftOuterInterpConfig i j hji z.1 z.2) := by sorry

end TarchaBraids
Source
Modular continuity lift for Tarcha's explicit adjacent Artin relation homotopy.

View graph