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

theorem StrongExchangeBridge.exchange_descent_eraseIdx {W : Type u_1} [Group W] {B : Type u_2} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (hsce : CoxeterExchange.SignChangeExchangeHyp M cs) (word : List B) (s : B) (hred : cs.IsReduced word) (hdesc : cs.length (cs.wordProd word * cs.simple s) < cs.length (cs.wordProd word)) : ∃ (i : Fin word.length), cs.wordProd (word.eraseIdx ↑i) = cs.wordProd word * cs.simple s ∧ cs.IsReduced (word.eraseIdx ↑i)

Exchange via erase-index: when $s$ is a right descent of a reduced word $w$, there is an index $i$ such that erasing it yields a reduced word with product $w \cdot s$.

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

theorem StrongExchangeBridge.exists_reduced_ending_in {W : Type u_1} [Group W] {B : Type u_2} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (hsce : CoxeterExchange.SignChangeExchangeHyp M cs) (word : List B) (s : B) (hred : cs.IsReduced word) (hdesc : cs.length (cs.wordProd word * cs.simple s) < cs.length (cs.wordProd word)) : ∃ (prefix_word : List B), cs.IsReduced (prefix_word ++ [s]) ∧ cs.wordProd (prefix_word ++ [s]) = cs.wordProd word ∧ prefix_word.length + 1 = word.length

Existence of a reduced word ending in $s$: if $s$ is a right descent of a reduced word $w$, there is a reduced word $w' \cdot s$ of the same product.

theorem StrongExchangeBridge.exists_reduced_word_ending_in_descent {W : Type u_1} [Group W] {B : Type u_2} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (w : W) (s : B) (hdesc : cs.length (w * cs.simple s) < cs.length w) : ∃ (prefix_word : List B), cs.IsReduced (prefix_word ++ [s]) ∧ cs.wordProd (prefix_word ++ [s]) = w

If $s$ is a right descent of $w$, then $w$ has a reduced word ending in $s$.