Tarcha 3.15 adjacent raw maps are coordinatewise continuous

Proved

TarchaBraids.thm_3_15_adjacent_raw_continuous_v1

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

artin-presentationbraid-groupscontinuitytarcha

Each strand coordinate of the left and right adjacent braid-word paths and of the common outer-rotation path varies continuously in the path parameter.

Preamble

import Mathlib
import Definitions.Def_TarchaBraids_adjacent_path_data_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_adjacent_raw_continuous_v1 :
    (∀ (n : ℕ) (i j : Fin (n - 1)) (k : Fin n),
      Continuous (fun q : ℝ => leftBraidFun n i j q k)) ∧
    (∀ (n : ℕ) (i j : Fin (n - 1)) (k : Fin n),
      Continuous (fun q : ℝ => rightBraidFun n i j q k)) ∧
    (∀ (n : ℕ) (i : Fin (n - 1)) (k : Fin n),
      Continuous (fun q : ℝ => outerRotateFun n i q k)) := by sorry

end TarchaBraids

Source

Modular extraction of the coordinate-continuity layer from the explicit adjacent Artin relation proof.

View graph