Prove2Me

Tarcha 3.15 adjacent ordered configuration paths are continuous

Proved
TarchaBraids.thm_3_15_adjacent_config_continuous_v1

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

artin-presentationbraid-groupscontinuitytarcha

The ordered-configuration lifts of the left adjacent braid word, right adjacent braid word and outer-rotation comparison path are continuous.

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

open BraidsLinksMCG

theorem thm_3_15_adjacent_config_continuous_v1 :
    (∀ (n : ℕ) (i j : Fin (n - 1)), Continuous (leftBraidConfig n i j)) ∧
    (∀ (n : ℕ) (i j : Fin (n - 1)), Continuous (rightBraidConfig n i j)) ∧
    (∀ {n : ℕ} (i : Fin (n - 1)) (hi2 : (i : ℕ) + 2 < n),
      Continuous (outerRotateConfig i hi2)) := by sorry

end TarchaBraids
Source
Modular lift of the accepted raw coordinatewise continuity theorem through the ordered-configuration subtype.

View graph