@[reducible, inline]

abbrev CoxeterExchange.SignChangeExchangeHyp {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : Prop

The sign-change exchange hypothesis: whenever a reduced word $\omega$ makes $e_s$ into a negative root, there is some position $i$ in $\omega$ such that deleting it gives a word with product $\mathtt{wordProd}\,\omega \cdot \mathtt{simple}\,s$.

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

def CoxeterExchange.geometricBridgeFromNegOfDescent {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (hsce : SignChangeExchangeHyp M cs) : CoxeterExchangeGenuine.GeometricBridgeHyp M cs

Deprecated bridge construction: builds the geometric bridge hypothesis from a sign-change exchange hypothesis together with the length-decrease implies negativity lemma.

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

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

Deprecated wrapper: the sign-change exchange hypothesis implies the abstract exchange condition.