The strand-index adjacent swaps give a surjective free-group lift

Proved

TarchaBraids.strandIdx_swap_free_lift_surjective_v1

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

adjacent-transpositionsbraid-groupsfree-groupsindexingpermutationstarcha

For n labelled strands, every endpoint permutation is represented by a signed word in the adjacent swaps indexed exactly as the braid generators, using strandIdx i and strandIdxSucc i. This is the indexing bridge from the standard Fin m adjacent-swap theorem to the form required by the half-twist permutation-correction theorem.

Preamble

import Mathlib
import Definitions.Def_BraidsLinksMCG_ArtinEndo
import Theorems.Thm_TarchaBraids_adjacent_swap_free_lift_surjective_v1

Formal statement

namespace TarchaBraids

open BraidsLinksMCG

theorem strandIdx_swap_free_lift_surjective_v1 (n : ℕ) :
    Function.Surjective
      (FreeGroup.lift (fun i : Fin (n - 1) =>
        Equiv.swap (strandIdx i) (strandIdxSucc i))) := by sorry

end TarchaBraids

Source

Tarcha Teorema 3.11 endpoint-permutation correction. This child translates the already proved adjacent-transposition generation theorem into the exact strandIdx/strandIdxSucc indexing used by the geometric half-twists.

View graph