Tarcha 3.15 outer rotation has the common q=1 endpoint

Proved

TarchaBraids.thm_3_15_adjacent_outer_one_endpoint_v1

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

artin-presentationbraid-groupsendpointstarcha

For adjacent strands with the required third local strand, the explicit outer-rotation comparison path ends at the same outer-strand transposition of the ordered base configuration.

Preamble

import Mathlib
import Definitions.Def_TarchaBraids_adjacent_path_data_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_adjacent_outer_one_endpoint_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1)
      (hi2 : (i : ℕ) + 2 < n),
      outerRotateFun n i 1 =
        (baseOrdered n).1 ∘ Equiv.swap (strandIdx i) (strandIdxSucc j) := by sorry

end TarchaBraids

Source

Modular q=1 outer-rotation endpoint extraction from the explicit adjacent Artin relation proof.

View graph