Tarcha 3.15 right interpolation q=1 endpoint permutation

Proved

TarchaBraids.thm_3_15_right_interp_one_fun_v1

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

artin-presentationbraid-groupshomotopytarcha

At q=1 every point of the right interpolation is the same endpoint configuration, namely the base ordered configuration with the two outer local strands swapped.

Preamble

import Mathlib
import Definitions.Def_TarchaBraids_right_interp_config_data_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_word_one_endpoints_v1
import Theorems.Thm_TarchaBraids_thm_3_15_adjacent_outer_one_endpoint_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem thm_3_15_right_interp_one_fun_v1 :
    ∀ {n : ℕ} (i j : Fin (n - 1)) (hji : (j : ℕ) = (i : ℕ) + 1)
      (u : unitInterval),
      (rightOuterInterpConfig i j hji u 1).1 =
        (baseOrdered n).1 ∘ Equiv.swap (strandIdx i) (strandIdxSucc j) := by sorry

end TarchaBraids

Source

Modular remaining adjacent-relation proof for Tarcha 3.15.

View graph