Finite signed half-twist words for Tarcha generation

import Mathlib
import Definitions.Def_BraidsLinksMCG_ConfigSpace
import Definitions.Def_TarchaBraids_HalfTwist

/-!
# Finite signed half-twist words

Reusable signed-word data for the generation branch.

The list order is algebraic order. Because the pinned fundamental group uses
`p * q = q.trans p`, path concatenation is reversed relative to multiplication.
-/

namespace TarchaBraids

open BraidsLinksMCG

noncomputable section

inductive BraidLetterSign where
  | positive
  | negative
  deriving DecidableEq

structure BraidLetter (n : ℕ) where
  index : Fin (n - 1)
  sign : BraidLetterSign
  deriving DecidableEq

def braidLetterFree {n : ℕ} (a : BraidLetter n) : FreeGroup (Fin (n - 1)) :=
  match a.sign with
  | .positive => FreeGroup.of a.index
  | .negative => (FreeGroup.of a.index)⁻¹

def braidLetterLoop (n : ℕ) (a : BraidLetter n) :
    Path (baseUnordered n) (baseUnordered n) :=
  match a.sign with
  | .positive => halfTwistLoop n a.index
  | .negative => (halfTwistLoop n a.index).symm

def braidWordFree {n : ℕ} : List (BraidLetter n) → FreeGroup (Fin (n - 1))
  | [] => 1
  | a :: w => braidLetterFree a * braidWordFree w

def braidWordLoop (n : ℕ) : List (BraidLetter n) →
    Path (baseUnordered n) (baseUnordered n)
  | [] => Path.refl (baseUnordered n)
  | a :: w => (braidWordLoop n w).trans (braidLetterLoop n a)

/-- Path-level normal form needed for Tarcha's generation theorem. -/
def EveryLoopHasBraidWord (n : ℕ) : Prop :=
  ∀ γ : Path (baseUnordered n) (baseUnordered n),
    ∃ w : List (BraidLetter n), Path.Homotopic γ (braidWordLoop n w)

end

end TarchaBraids