Tarcha 3.15 right adjacent first-phase local coordinate facts

Proved

TarchaBraids.thm_3_15_adjacent_right_first_local_facts_v1

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

artin-presentationbraid-groupsgeometrysymmetrytarcha

In the first 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_first_local_facts_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1),
      (∀ (q : ℝ), q ≤ 1 / 2 →
        rightBraidFun n i j q (strandIdx i) = ((((i : ℕ) : ℝ) + 1 : ℝ) : ℂ)) ∧
      (∀ (q : ℝ), q ≤ 1 / 2 →
        rightBraidFun n i j q (strandIdxSucc i) =
          twistPoint ((i : ℕ) + 5 / 2) (-1) (2 * q)) ∧
      (∀ (q : ℝ), q ≤ 1 / 2 →
        rightBraidFun n i j q (strandIdxSucc j) =
          twistPoint ((i : ℕ) + 5 / 2) 1 (2 * q)) := by sorry

end TarchaBraids

Source

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

View graph