theorem CoxeterGroup.wordSigma_of_supported_two {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (word : List B) (v : B → ℝ) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) : wordSigma M word v = fun (u : B) => v s * wordSigma M word (e s) u + v t * wordSigma M word (e t) u

Pointwise linearity of $\sigma_w$ on vectors supported in $\{s, t\}$: $\sigma_w(v)(u) = v_s \cdot \sigma_w(\alpha_s)(u) + v_t \cdot \sigma_w(\alpha_t)(u)$.

theorem CoxeterGroup.pos_of_ascent_case_b {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (n : ℕ) (ih : ∀ m < n, ∀ (word : List B) (s : B), word.length = m → cs.IsReduced word → cs.length (cs.wordProd word * cs.simple s) > cs.length (cs.wordProd word) → IsPositive (wordSigma M word (e s))) (init : List B) (s t : B) (hts : t ≠ s) (hred_init : cs.IsReduced init) (hasc_t : cs.length (cs.wordProd init * cs.simple t) > cs.length (cs.wordProd init)) (hdesc_s : cs.length (cs.wordProd init * cs.simple s) < cs.length (cs.wordProd init)) (hasc : cs.length (cs.wordProd (init ++ [t]) * cs.simple s) > cs.length (cs.wordProd (init ++ [t]))) (hinit_len : init.length < n) : IsPositive (wordSigma M (init ++ [t]) (e s))

Inductive step (Case B) of the positivity-on-ascent argument: handles the case where $t$ ascends $w$ on the right but $s$ descends $w$. The argument reduces to a smaller word via parabolic decomposition.

theorem CoxeterGroup.pos_of_ascent_proof {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (n : ℕ) (word : List B) (s : B) : word.length = n → cs.IsReduced word → cs.length (cs.wordProd word * cs.simple s) > cs.length (cs.wordProd word) → IsPositive (wordSigma M word (e s))

Strong-induction proof of positivity on ascent: if $w$ is reduced and $s$ ascends $w$ on the right, then $\sigma_w(\alpha_s)$ is a positive vector.

theorem CoxeterGroup.pos_of_ascent {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) (hasc : cs.length (cs.wordProd word * cs.simple s) > cs.length (cs.wordProd word)) : IsPositive (wordSigma M word (e s))

Positivity on ascent: for a reduced word $w$ with $\ell(ws) > \ell(w)$, the vector $\sigma_w(\alpha_s)$ is positive.

theorem CoxeterGroup.neg_of_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) (hdesc : cs.length (cs.wordProd word * cs.simple s) < cs.length (cs.wordProd word)) : IsNegative (wordSigma M word (e s))

Negativity on descent: for a reduced word $w$ with $\ell(ws) < \ell(w)$, the vector $\sigma_w(\alpha_s)$ is negative.