theorem CoxeterGroup.alternatingWord_chain' {B : Type u_1} [DecidableEq B] [Fintype B] (s t : B) (hst : s ≠ t) (n : ℕ) : List.Chain' (fun (x1 x2 : B) => x1 ≠ x2) (CoxeterSystem.alternatingWord s t n)

The alternating word $s\,t\,s\,t\,\cdots$ in two distinct generators has no two consecutive equal letters: it is a $\mathtt{Chain'}$ for $(\ne)$.

theorem CoxeterGroup.alternatingWord_last_cond {B : Type u_1} [DecidableEq B] [Fintype B] (s t : B) (n : ℕ) : CoxeterSystem.alternatingWord s t n = [] ∨ ∃ (h : CoxeterSystem.alternatingWord s t n ≠ []), (CoxeterSystem.alternatingWord s t n).getLast h = t

The alternating word $s\,t\,s\,t\,\cdots$ either is empty or ends in $t$ (since each step in the recursion of $\mathtt{alternatingWord}$ appends $t$ at the right).

theorem CoxeterGroup.alternatingWord_pos {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (n : ℕ) (hlen : n < M.M s t ∨ M.M s t = 0) : IsPositive (wordSigma M (CoxeterSystem.alternatingWord s t n) (e s))

Positivity of the dihedral iterate along an alternating word: for any $n < m(s, t)$ (or $m(s, t) = \infty$), the action of the alternating word $\mathtt{alternatingWord}\,s\,t\,n$ on $e_s$ via $\sigma$ produces a positive root.

theorem CoxeterGroup.wordSigma_pos_of_word_in_two {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) {W : Type u_2} [Group W] (cs : CoxeterSystem M W) (s t : B) (hst : s ≠ t) (word : List B) (hmem : ∀ b ∈ word, b = s ∨ b = t) (hlen : cs.length (cs.wordProd word) < M.M s t ∨ M.M s t = 0) (hform : ∃ (n : ℕ), cs.wordProd word = cs.wordProd (CoxeterSystem.alternatingWord s t n) ∧ (n < M.M s t ∨ M.M s t = 0)) : IsPositive (wordSigma M word (e s))

Generalisation to arbitrary words in two generators: any word whose product equals that of some alternating word of admissible length yields a positive iterate of $e_s$ under $\mathtt{wordSigma}$.