Tarcha 3.15 right and left adjacent braid path reflection

Proved

TarchaBraids.thm_3_15_adjacent_right_left_braid_reflection_v1

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

artin-presentationbraid-groupsgeometrysymmetrytarcha

The three distinguished strands of the right adjacent braid word are the reflections of the corresponding left-word strands about the centre with real coordinate i+2.

Preamble

import Mathlib
import Definitions.Def_TarchaBraids_adjacent_path_data_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_left_local_facts_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_right_first_local_facts_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_right_middle_local_facts_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_right_final_local_facts_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_adjacent_right_left_braid_reflection_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
      (∀ q : ℝ,
        rightBraidFun n i j q (strandIdx i) =
          (((2 * (((i : ℕ) : ℝ) + 2) : ℝ) : ℂ) -
            leftBraidFun n i j q (strandIdxSucc j))) ∧
      (∀ q : ℝ,
        rightBraidFun n i j q (strandIdxSucc i) =
          (((2 * (((i : ℕ) : ℝ) + 2) : ℝ) : ℂ) -
            leftBraidFun n i j q (strandIdxSucc i))) ∧
      (∀ q : ℝ,
        rightBraidFun n i j q (strandIdxSucc j) =
          (((2 * (((i : ℕ) : ℝ) + 2) : ℝ) : ℂ) -
            leftBraidFun n i j q (strandIdx i))) := by sorry

end TarchaBraids

Source

Phasewise right/left reflection assembled from accepted modular local-coordinate theorems.

View graph