theorem StrongExchangeUnconditional.isReduced_of_append_isReduced {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (word : List B) (s : B) (h : cs.IsReduced (word ++ [s])) : cs.IsReduced word

If $\omega \cdot s$ is a reduced word, so is its prefix $\omega$.

theorem StrongExchangeUnconditional.not_descent_length_eq {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (v : W) (i : B) (h : ¬cs.IsRightDescent v i) : cs.length (v * cs.simple i) = cs.length v + 1

If $i$ is not a right descent of $v$ then $\ell(vs_i) = \ell(v) + 1$.

theorem StrongExchangeUnconditional.descent_length_eq {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B) (h : cs.IsRightDescent w i) : cs.length (w * cs.simple i) + 1 = cs.length w

If $i$ is a right descent of $w$ then $\ell(ws_i) + 1 = \ell(w)$.

theorem StrongExchangeUnconditional.reflection_identification_core {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v w t : M.Group) (ht : t ∈ CoxeterBruhat.reflections M M.toCoxeterSystem) (hvt : v * t = w) (hlen : M.toCoxeterSystem.length v + 1 = M.toCoxeterSystem.length w) (i : B) (hv_asc : ¬M.toCoxeterSystem.IsRightDescent v i) (hw_desc : M.toCoxeterSystem.IsRightDescent w i) : t = M.toCoxeterSystem.simple i

Reflection identification (core): in a Bruhat cover $v \lessdot w = vt$ where $i$ is a descent of $w$ but not of $v$, the reflection $t$ must be the simple reflection $s_i$. This is the geometric core of the strong exchange theorem.

theorem StrongExchangeUnconditional.inversionDifferenceBridge_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : CoxeterReflectionId.InversionDifferenceBridgeHyp M.toCoxeterSystem

Unconditional inversion-difference bridge: the reflection identification core packaged.

theorem StrongExchangeUnconditional.reflectionIdentificationHyp_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : CoxeterBruhat.ReflectionIdentificationHyp M.toCoxeterSystem

Unconditional reflection identification hypothesis for any Coxeter matrix.

theorem StrongExchangeUnconditional.strongExchangeForBruhat_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : CoxeterBruhat.StrongExchangeForBruhat M.toCoxeterSystem

Unconditional strong exchange theorem for the Bruhat order: any Coxeter system satisfies the strong exchange condition.