def CoxeterSystemFromDeletion.HTypeEq {W' : Type u_1} [Monoid W'] (g : ℕ → W') (m k : ℕ) : Prop

The "$H$-equation" at rotation $k$: $\prod_{i=k+1}^{k+m} g_i = \prod_{i=k}^{k+m-1} g_i$.

def CoxeterSystemFromDeletion.AllRotationsUnlucky {W' : Type u_1} [Monoid W'] (g : ℕ → W') (m : ℕ) : Prop

The "unlucky" case: the $H$-equation holds at every cyclic rotation $k$.

theorem CoxeterSystemFromDeletion.all_unlucky_implies_Ltype {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) (hDel : SatisfiesDeletionConditionGen gen) (word : List B) (hw : (List.map gen word).prod = 1) (m : ℕ) (hlen : word.length = 2 * m) (hm : m ≥ 2) (h_all_unlucky : AllRotationsUnlucky (wordCyclicGen gen word (2 * m) hlen ⋯) m) (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)

In the unlucky case, every length-$m$ window product takes the special "$L$-type" form $g_{k+2} \cdot g_{k+1} \cdot \prod_{k+2}^{k+m-1} g$.

theorem CoxeterSystemFromDeletion.all_unlucky_implies_alternating {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) (hDel : SatisfiesDeletionConditionGen gen) (word : List B) (hw : (List.map gen word).prod = 1) (m : ℕ) (hlen : word.length = 2 * m) (hm : m ≥ 2) (h_all_unlucky : AllRotationsUnlucky (wordCyclicGen gen word (2 * m) hlen ⋯) m) (k : ℕ) (x✝ : k + 2 < word.length) : gen (word.get ⟨k, ⋯⟩) = gen (word.get ⟨k + 2, x✝⟩)

In the unlucky case, the generator values are $2$-periodic: $\mathrm{gen}(w_k) = \mathrm{gen}(w_{k+2})$.

theorem CoxeterSystemFromDeletion.all_unlucky_implies_alternating_Blevel {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) (hDel : SatisfiesDeletionConditionGen gen) (word : List B) (hw : (List.map gen word).prod = 1) (m : ℕ) (hlen : word.length = 2 * m) (hm : m ≥ 2) (h_all_unlucky : AllRotationsUnlucky (wordCyclicGen gen word (2 * m) hlen ⋯) m) (k : ℕ) (hk : k + 2 < word.length) : word.get ⟨k, ⋯⟩ = word.get ⟨k + 2, hk⟩

Lifted to the alphabet $B$: in the unlucky case, $w_k = w_{k+2}$ in $B$ (not just at the generator level), using injectivity of $\mathrm{gen}$.

theorem CoxeterSystemFromDeletion.alternating_word_prod_eq_pow_local {B' : Type u_1} {G : Type u_2} [Group G] (f : B' → G) (word : List B') (m : ℕ) (hlen : word.length = 2 * m) (hm : m ≥ 1) (halt : ∀ (k : ℕ) (hk : k + 2 < word.length), word.get ⟨k, ⋯⟩ = word.get ⟨k + 2, hk⟩) : (List.map f word).prod = (f (word.get ⟨0, ⋯⟩) * f (word.get ⟨1, ⋯⟩)) ^ m

For a length-$2m$ word that is $2$-periodic, the product factors as $(f(w_0) f(w_1))^m$.