Tarcha 3.15 right adjacent middle-phase local coordinate facts

Proved

TarchaBraids.thm_3_15_adjacent_right_middle_local_facts_v1

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

artin-presentationbraid-groupsgeometrysymmetrytarcha

In the middle phase of the right adjacent three-half-twist word, the three distinguished strands have the stated explicit coordinates.

Preamble

import Mathlib
import Definitions.Def_TarchaBraids_adjacent_path_data_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_adjacent_right_middle_local_facts_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
      (∀ (q : ℝ), ¬ q ≤ 1 / 2 → q ≤ 3 / 4 →
        rightBraidFun n i j q (strandIdx i) =
          twistPoint ((i : ℕ) + 3 / 2) (-1) (4 * q - 2)) ∧
      (∀ (q : ℝ), ¬ q ≤ 1 / 2 → q ≤ 3 / 4 →
        rightBraidFun n i j q (strandIdxSucc i) = ((((i : ℕ) : ℝ) + 3 : ℝ) : ℂ)) ∧
      (∀ (q : ℝ), ¬ q ≤ 1 / 2 → q ≤ 3 / 4 →
        rightBraidFun n i j q (strandIdxSucc j) =
          twistPoint ((i : ℕ) + 3 / 2) 1 (4 * q - 2)) := by sorry

end TarchaBraids

Source

Middle phase extracted from the failed monolithic right-reflection child.

View graph