Prove2Me

Tarcha 3.15 right adjacent final-phase local coordinate facts

Proved
TarchaBraids.thm_3_15_adjacent_right_final_local_facts_v1

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

artin-presentationbraid-groupsgeometrysymmetrytarcha

In the final 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_final_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 : ℕ) + 5 / 2) (-1) (4 * q - 3)) ∧
      (∀ (q : ℝ), ¬ q ≤ 1 / 2 → ¬ q ≤ 3 / 4 →
        rightBraidFun n i j q (strandIdxSucc i) =
          twistPoint ((i : ℕ) + 5 / 2) 1 (4 * q - 3)) ∧
      (∀ (q : ℝ), ¬ q ≤ 1 / 2 → ¬ q ≤ 3 / 4 →
        rightBraidFun n i j q (strandIdxSucc j) = ((((i : ℕ) : ℝ) + 1 : ℝ) : ℂ)) := by sorry

end TarchaBraids
Source
Final phase extracted from the failed monolithic right-reflection child.

View graph