theorem CoxeterSignChangeExchangeFinal.isPositive_isNegative_eq_zero {B : Type u_1} [DecidableEq B] [Fintype B] {v : B → ℝ} (hpos : CoxeterGroup.IsPositive v) (hneg : CoxeterGroup.IsNegative v) : v = 0

A vector that is both positive and negative everywhere is zero.

theorem CoxeterSignChangeExchangeFinal.bilinForm_zero_left {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (w : B → ℝ) : CoxeterGroup.bilinForm M 0 w = 0

The bilinear form vanishes when its left argument is zero.

theorem CoxeterSignChangeExchangeFinal.isReduced_drop' {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {word : List B} (hred : cs.IsReduced word) (j : ℕ) : cs.IsReduced (List.drop j word)

Convenience wrapper: dropping a prefix of a reduced word leaves a reduced word.

theorem CoxeterSignChangeExchangeFinal.e_not_isNegative {B : Type u_1} [DecidableEq B] [Fintype B] (s : B) : ¬CoxeterGroup.IsNegative (CoxeterGroup.e s)

The simple root $e_s$ is not negative (its $s$-coordinate is $1 > 0$).

theorem CoxeterSignChangeExchangeFinal.isNegative_implies_descent {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) (hred : cs.IsReduced word) (hneg : CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e s))) : cs.length (cs.wordProd word * cs.simple s) < cs.length (cs.wordProd word)

If $w \cdot e_s$ is negative for a reduced word $w$, then $s$ is a right descent: $\ell(ws) < \ell(w)$.

theorem CoxeterSignChangeExchangeFinal.coxeterRepresentation_injective {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) {W : Type u_2} [Group W] (cs : CoxeterSystem M W) : Function.Injective ⇑(CoxeterGroup.coxeterRepresentation M cs)

Faithfulness of the geometric (Tits) representation: the homomorphism $W \to \operatorname{GL}(\mathbb{R}^B)$ given by simple reflections is injective.

theorem CoxeterSignChangeExchangeFinal.isPositive_sigma_isNegative_eq_e {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (t : B) (v : B → ℝ) (hpos : CoxeterGroup.IsPositive v) (hneg_sigma : CoxeterGroup.IsNegative (CoxeterGroup.sigma M t v)) (hform : CoxeterGroup.bilinForm M v v = 1) : v = CoxeterGroup.e t

If $v$ is positive, $\sigma_t v$ is negative, and $\langle v, v\rangle = 1$, then $v = e_t$. This is the geometric "unique root" step that powers the sign-change exchange.

theorem CoxeterSignChangeExchangeFinal.wordProd_cons_eq_append_of_wordSigma_eq_e {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (tail : List B) (s t : B) (hsigma : CoxeterGroup.wordSigma M tail (CoxeterGroup.e s) = CoxeterGroup.e t) : cs.simple t * cs.wordProd tail = cs.wordProd tail * cs.simple s

If $w \cdot e_s = e_t$ geometrically, then $s_t \cdot w = w \cdot s_s$ in the Coxeter group.

theorem CoxeterSignChangeExchangeFinal.exchange_at_zero {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (t : B) (tail : List B) (s : B) (hsigma : CoxeterGroup.wordSigma M tail (CoxeterGroup.e s) = CoxeterGroup.e t) : cs.wordProd tail = cs.wordProd (t :: tail) * cs.simple s

Exchange at the leading position: if $\mathrm{tail} \cdot e_s = e_t$, deleting the head $t$ realizes the exchange $w_{\text{tail}} = (t :: \mathrm{tail}) \cdot s$.

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

Sign change exchange theorem (unconditional): if a reduced word $w$ satisfies $w \cdot e_s$ is negative, then there is an index $i$ such that $w' \cdot s = w$ where $w'$ is $w$ with its $i$-th letter removed. This is the geometric form of the exchange condition.