def CoxeterExchange.SatisfiesExchangeCondition {B : Type u_1} {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : Prop

Exchange Condition for $(W, S)$: for every reduced word $s_1 \cdots s_k$ and every generator $s$ with $\ell(w s) < \ell(w)$, there exists an index $i$ such that $s_1 \cdots \widehat{s_i} \cdots s_k = ws$.

def CoxeterExchange.SatisfiesDeletionCondition {B : Type u_1} {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : Prop

Deletion Condition for $(W, S)$: any non-reduced word $s_1 \cdots s_k$ (i.e. $\ell(\prod s_i) < k$) admits two indices $i < j$ that can be deleted without changing the product.

def CoxeterExchange.ExchangeCorollary {B : Type u_1} {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : Prop

Corollary of the Exchange Condition: if $s, t \in S$ are ascents on both sides of $w$, then either $\ell(swt) = \ell(w) + 2$ or $swt = w$.

theorem CoxeterExchange.exists_first_decreasing (f : ℕ → ℕ) (n : ℕ) (h0 : f 0 = 0) (hstep : ∀ j < n, f (j + 1) = f j + 1 ∨ f (j + 1) + 1 = f j) (hlt : n > f n) : ∃ j < n, f (j + 1) + 1 = f j ∧ ∀ k < j, f (k + 1) = f k + 1

Auxiliary combinatorial lemma: if $f : \mathbb{N} \to \mathbb{N}$ starts at $0$ and each step is $\pm 1$, then below any $n$ with $f(n) < n$ there is a first index where $f$ decreases.

@[deprecated "Use deletion_unconditional from UnconditionalExchange.lean" (since := "2025-01-01")]

theorem CoxeterExchange.deletion_of_exchange {B : Type u_2} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hex : SatisfiesExchangeCondition M cs) : SatisfiesDeletionCondition M cs

Exchange $\Rightarrow$ Deletion: under the Exchange Condition, any non-reduced word admits a deletion of two letters preserving the product.

@[deprecated "Use corollary_unconditional from UnconditionalExchange.lean" (since := "2025-01-01")]

theorem CoxeterExchange.corollary_of_exchange {B : Type u_2} {W : Type u_3} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (hex : SatisfiesExchangeCondition M cs) : ExchangeCorollary M cs

Two-sided ascent corollary derived from the Exchange Condition: if $s, t$ ascend $w$ on both sides then either $\ell(swt) = \ell(w) + 2$ or $swt = w$.