The classical pure half-twist word for a standard punctured-plane loop

import Mathlib
import Definitions.Def_TarchaBraids_generation_word_data_v1

/-!
# The classical pure braid word for a punctured-plane standard loop

For the standard loop in which the last strand encircles puncture `j`, the
classical Artin word is

`σ_{n-1} ... σ_{j+1} σ_j^2 σ_{j+1}^{-1} ... σ_{n-1}^{-1}`

in zero-based generator indexing.
-/

namespace TarchaBraids

noncomputable section

/-- The signed adjacent-generator word for the pure braid in which the last
strand encircles puncture `j`. The list is in algebraic multiplication order. -/
def standardPureBraidWord (n : ℕ) (j : Fin n) : List (BraidLetter (n + 1)) :=
  let higher := (List.finRange n).filter (fun k => j < k)
  let positive : Fin n → BraidLetter (n + 1) := fun k =>
    { index := Fin.cast (by omega) k
      sign := .positive }
  let negative : Fin n → BraidLetter (n + 1) := fun k =>
    { index := Fin.cast (by omega) k
      sign := .negative }
  higher.reverse.map positive ++
    [positive j, positive j] ++
    higher.map negative

end

end TarchaBraids