theorem CoxeterSystem.wordProd_alternatingWord_periodic {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (n : ℕ) : cs.wordProd (alternatingWord i i' (n + M.M i i' * 2)) = cs.wordProd (alternatingWord i i' n)

Period-$2 m(i, i')$ identity for the alternating word product: extending an alternating word $s_i s_{i'} s_i \cdots$ by $2 m(i, i')$ extra letters does not change its product in $W$.

theorem CoxeterSystem.length_wordProd_alternatingWord_le {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (n : ℕ) (hM : M.M i i' ≠ 0) : cs.length (cs.wordProd (alternatingWord i i' n)) ≤ M.M i i'

Length bound for alternating word products in the dihedral subgroup: $\ell(\pi(\mathtt{alternatingWord}\,i\,i'\,n)) \le m(i, i')$ whenever $m(i, i') \ne 0$.

theorem CoxeterSystem.wordProd_alternatingWord_mul_simple {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (n : ℕ) : cs.wordProd (alternatingWord i i' n) * cs.simple i = cs.wordProd (alternatingWord i' i (n + 1))

Right multiplication by $s_i$ extends an alternating word $s_i s_{i'} \cdots$ of length $n$ to an alternating word $s_{i'} s_i \cdots$ of length $n + 1$.

theorem CoxeterSystem.wordProd_alternatingWord_mul_same {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (n : ℕ) : cs.wordProd (alternatingWord i' i (n + 1)) * cs.simple i = cs.wordProd (alternatingWord i i' n)

Right multiplication by $s_i$ shortens an alternating word $s_{i'} s_i \cdots$ of length $n + 1$ ending in $s_i$ to the alternating word $s_i s_{i'} \cdots$ of length $n$.

theorem CoxeterSystem.wordProd_word_in_two_generators {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (word : List B) (hmem : ∀ b ∈ word, b = i ∨ b = i') : ∃ (n : ℕ), cs.wordProd word = cs.wordProd (alternatingWord i i' n) ∨ cs.wordProd word = cs.wordProd (alternatingWord i' i n)

Any word in two simple generators $s_i, s_{i'}$ has the same product as some alternating word in those generators (starting with either letter).

theorem CoxeterSystem.length_wordProd_le_M {B : Type u_1} {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i i' : B) (word : List B) (hmem : ∀ b ∈ word, b = i ∨ b = i') (hM : M.M i i' ≠ 0) : cs.length (cs.wordProd word) ≤ M.M i i'

Universal dihedral length bound: any word in the two simple generators $s_i, s_{i'}$ has product of length at most $m(i, i')$.