theorem CoxeterExchange.exchange_condition_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : SatisfiesExchangeCondition M cs

Unconditional exchange condition for any Coxeter system.

theorem CoxeterExchange.deletion_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : SatisfiesDeletionCondition M cs

Unconditional deletion condition for any Coxeter system.

theorem CoxeterExchange.corollary_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : ExchangeCorollary M cs

The corollary of the exchange condition, made unconditional.

theorem CoxeterExchange.all_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : SatisfiesExchangeCondition M cs ∧ SatisfiesDeletionCondition M cs ∧ ExchangeCorollary M cs

Combined: the exchange condition, deletion condition, and exchange corollary all hold unconditionally for any Coxeter system.

theorem CoxeterExchange.exchange_implies_deletion_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : SatisfiesDeletionCondition M cs

Exchange ⇒ deletion, applied unconditionally via the sign-change hypothesis.

theorem CoxeterExchange.exchange_implies_corollary_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : ExchangeCorollary M cs

Exchange ⇒ corollary, applied unconditionally.

theorem CoxeterExchange.exchange_implies_both_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) : SatisfiesDeletionCondition M cs ∧ ExchangeCorollary M cs

Exchange ⇒ both deletion and corollary, packaged unconditionally.

theorem StrongExchangeBridge.exchange_descent_eraseIdx_unconditional {W : Type u_1} [Group W] {B : Type u_2} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (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)

Unconditional exchange-by-erase: removing an index from a reduced word with $s$ a right descent yields a reduced word with product $w \cdot s$.

theorem StrongExchangeBridge.exists_reduced_ending_in_unconditional {W : Type u_1} [Group W] {B : Type u_2} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (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

Unconditional version: when $s$ is a right descent, there is a reduced word ending in $s$ with the same product.