theorem CoxeterSystemFromDeletion.eraseIdx_eraseIdx_length {α : Type u_3} {l : List α} {i j : ℕ} (hij : i < j) (hj : j < l.length) : ((l.eraseIdx j).eraseIdx i).length + 2 = l.length

Erasing two distinct indices reduces the list length by exactly $2$: $|(l.\mathtt{eraseIdx}\,j).\mathtt{eraseIdx}\,i| + 2 = |l|$.

theorem CoxeterSystemFromDeletion.deletion_relation_even_length {B : Type u_3} {W : Type u_4} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (hDel : SatisfiesDeletionConditionGen gen) (word : List B) (hw : (List.map gen word).prod = 1) : Even word.length

If the family $\mathtt{gen}$ satisfies the deletion condition, any word mapping to $1$ under $\mathtt{gen}$ has even length. (One can repeatedly delete pairs of letters by the deletion condition.)

theorem CoxeterSystemFromDeletion.inv_eq_self_of_involution {G : Type u_3} [Group G] {g : G} (h : g * g = 1) : g⁻¹ = g

An involution is self-inverse: if $g \cdot g = 1$ then $g^{-1} = g$.

theorem CoxeterSystemFromDeletion.map_inv_eq_self_of_involutions {B : Type u_1} {W : Type u_2} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (l : List B) : List.map (fun (x : W) => x⁻¹) (List.map gen l) = List.map gen l

Mapping inversion over a list of involutions yields the same list.

theorem CoxeterSystemFromDeletion.reverse_map_prod_inv_of_involutions {B : Type u_1} {W : Type u_2} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (l : List B) : (List.map gen l.reverse).prod = (List.map gen l).prod⁻¹

For a list of involutions, the product of the reversed list equals the inverse of the original product.

theorem CoxeterSystemFromDeletion.first_half_nonreduced {B : Type u_1} {W : Type u_2} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (word : List B) (m : ℕ) (hlen : word.length = 2 * m) (hm : m > 1) (hw : (List.map gen word).prod = 1) : ∃ (shorter : List B), shorter.length < (List.take (m + 1) word).length ∧ (List.map gen shorter).prod = (List.map gen (List.take (m + 1) word)).prod

If a word of length $2m$ with $m > 1$ maps to $1$, then its initial segment of length $m + 1$ admits a strictly shorter word with the same product: namely, the reverse of the second half.

theorem CoxeterSystemFromDeletion.alternating_word_maps_to_one {B : Type u_1} {W : Type u_2} [Group W] (gen : B → W) (hgen_inv : ∀ (s : B), gen s * gen s = 1) (hgen_ne : ∀ (s t : B), s ≠ t → gen s * gen t ≠ 1) (s t : B) (m : ℕ) (h_prod : (gen s * gen t) ^ m = 1) : have M := deletionCoxeterMatrix gen hgen_inv hgen_ne; (M.simple s * M.simple t) ^ m = 1

Transport of the braid relation: if $(\mathtt{gen}\,s \cdot \mathtt{gen}\,t)^m = 1$ in $W$, then the same braid relation $(\mathtt{simple}\,s \cdot \mathtt{simple}\,t)^m = 1$ holds in the abstract Coxeter group associated to $\mathtt{gen}$.

def CoxeterSystemFromDeletion.consecProd {W : Type u_3} [Monoid W] (g : ℕ → W) (k m : ℕ) : W

The product $g(k) \cdot g(k+1) \cdots g(k + m - 1)$ of $m$ consecutive values of a sequence $g : \mathbb{N} \to W$ starting at index $k$.

theorem CoxeterSystemFromDeletion.consecProd_succ {W' : Type u_3} [Monoid W'] (g : ℕ → W') (k m : ℕ) : consecProd g k (m + 1) = g k * consecProd g (k + 1) m

Peeling off the first factor: $\mathtt{consecProd}\,g\,k\,(m+1) = g(k) \cdot \mathtt{consecProd}\,g\,(k+1)\,m$.

theorem CoxeterSystemFromDeletion.consecProd_succ_succ {W' : Type u_3} [Monoid W'] (g : ℕ → W') (k m : ℕ) : consecProd g k (m + 2) = g k * g (k + 1) * consecProd g (k + 2) m

Peeling off two factors: $\mathtt{consecProd}\,g\,k\,(m+2) = g(k)\,g(k+1) \cdot \mathtt{consecProd}\,g\,(k+2)\,m$.

theorem CoxeterSystemFromDeletion.cycling_alternating_of_L_type {W : Type u_2} [Group W] (g : ℕ → W) (m : ℕ) (hm : m ≥ 2) (h_L : ∀ (k : ℕ), consecProd g k m = g (k + 2) * g (k + 1) * consecProd g (k + 2) (m - 2)) (k : ℕ) : g k = g (k + 2)

If for every $k$ the $m$-fold product starting at $k$ equals the same product but with the first factor replaced by $g(k+2)$, then $g$ is two-step periodic: $g(k) = g(k+2)$ for all $k$.

def CoxeterSystemFromDeletion.wordCyclicGen {B : Type u_1} {W : Type u_2} (gen : B → W) (word : List B) (n : ℕ) (hn : word.length = n) (hn0 : n > 0) (k : ℕ) : W

Cyclic extension of $\mathtt{gen}\circ\mathtt{word}$ to all of $\mathbb{N}$: at index $k$ it returns the generator at position $k \bmod n$.

theorem CoxeterSystemFromDeletion.cycling_forces_alternating {B : Type u_3} {W : Type u_4} [Group W] (gen : B → W) (word : List B) (m : ℕ) (hlen : word.length = 2 * m) (hm : m ≥ 2) (h_L_type : ∀ (k : ℕ), consecProd (wordCyclicGen gen word (2 * m) hlen ⋯) k m = wordCyclicGen gen word (2 * m) hlen ⋯ (k + 2) * wordCyclicGen gen word (2 * m) hlen ⋯ (k + 1) * consecProd (wordCyclicGen gen word (2 * m) hlen ⋯) (k + 2) (m - 2)) (k : ℕ) (hk : k + 2 < word.length) : gen (word.get ⟨k, ⋯⟩) = gen (word.get ⟨k + 2, hk⟩)

For a word of length $2m$ ($m \ge 2$), if the cyclic generator satisfies the $L$-type identity, then the word is two-step periodic at the level of generator values: $\mathtt{gen}(\mathtt{word}[k]) = \mathtt{gen}(\mathtt{word}[k+2])$ whenever both indices fit.