theorem DescentInversionBridge.wordSigma_eq_of_wordProd_eq {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word₁ word₂ : List B) (h : cs.wordProd word₁ = cs.wordProd word₂) (v : B → ℝ) : CoxeterGroup.wordSigma M word₁ v = CoxeterGroup.wordSigma M word₂ v

If two words have the same product in $W$, they induce the same action on the geometric representation.

theorem DescentInversionBridge.descent_implies_isNegative {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word : List B) (i : B) (hred : cs.IsReduced word) (hdesc : cs.IsRightDescent (cs.wordProd word) i) : CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e i))

Right-descent implies negative root: if a reduced word ends with a right descent at $i$, then its action on $e_i$ is a negative root.

theorem DescentInversionBridge.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) (i : B) (hred : cs.IsReduced word) (hneg : CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e i))) : cs.IsRightDescent (cs.wordProd word) i

Converse: if a reduced word's action on $e_i$ is a negative root, then $i$ is a right descent of the corresponding group element.

theorem DescentInversionBridge.descent_iff_isNegative {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word : List B) (i : B) (hred : cs.IsReduced word) : cs.IsRightDescent (cs.wordProd word) i ↔ CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e i))

Descent-negativity equivalence for reduced words: $i$ is a right descent iff the word's action on $e_i$ gives a negative root.

theorem DescentInversionBridge.ascent_implies_isPositive {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word : List B) (i : B) (hred : cs.IsReduced word) (hasc : ¬cs.IsRightDescent (cs.wordProd word) i) : CoxeterGroup.IsPositive (CoxeterGroup.wordSigma M word (CoxeterGroup.e i))

Ascent implies positive root: if $i$ is not a right descent, the word's action on $e_i$ is a positive root.

theorem DescentInversionBridge.isPositive_implies_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) (i : B) (hred : cs.IsReduced word) (hpos : CoxeterGroup.IsPositive (CoxeterGroup.wordSigma M word (CoxeterGroup.e i))) : ¬cs.IsRightDescent (cs.wordProd word) i

Converse: if a reduced word's action on $e_i$ is a positive root, then $i$ is not a right descent.

theorem DescentInversionBridge.ascent_iff_isPositive {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word : List B) (i : B) (hred : cs.IsReduced word) : ¬cs.IsRightDescent (cs.wordProd word) i ↔ CoxeterGroup.IsPositive (CoxeterGroup.wordSigma M word (CoxeterGroup.e i))

Ascent-positivity equivalence for reduced words.

theorem DescentInversionBridge.wordSigma_append_isNegative_toggle {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) : CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M (word ++ [s]) (CoxeterGroup.e s)) ↔ CoxeterGroup.IsPositive (CoxeterGroup.wordSigma M word (CoxeterGroup.e s))

Appending $s$ to a word toggles negativity at $e_s$: the result is a negative root iff the original was a positive root.

theorem DescentInversionBridge.wordSigma_append_isPositive_toggle {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) : CoxeterGroup.IsPositive (CoxeterGroup.wordSigma M (word ++ [s]) (CoxeterGroup.e s)) ↔ CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e s))

The other direction: appending $s$ to a word toggles positivity at $e_s$.

theorem DescentInversionBridge.descent_toggle_append {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_word : cs.IsReduced word) (hred_app : cs.IsReduced (word ++ [s])) : cs.IsRightDescent (cs.wordProd (word ++ [s])) s ↔ ¬cs.IsRightDescent (cs.wordProd word) s

Right-descent toggle for an append: when both $\omega$ and $\omega \cdot s$ are reduced, $s$ is a right descent of $\omega s$ iff it is not a right descent of $\omega$.

theorem DescentInversionBridge.exists_reduced_word_ending_in_descent' {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (w : W) (s : B) (hdesc : cs.IsRightDescent w s) : ∃ (prefix_word : List B), cs.IsReduced (prefix_word ++ [s]) ∧ cs.wordProd (prefix_word ++ [s]) = w

For any right descent $s$ of $w$, there exists a reduced word for $w$ ending in $s$.

theorem DescentInversionBridge.descent_iff_isNegative_any_word {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (w : W) (word : List B) (s : B) (hred : cs.IsReduced word) (hprod : cs.wordProd word = w) : cs.IsRightDescent w s ↔ CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e s))

The descent-negativity equivalence stated in terms of a general representative reduced word.

theorem DescentInversionBridge.mem_bilinInversions_implies_isRightDescent {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) (hmem : s ∈ CoxeterGroup.bilinInversions M word) : cs.IsRightDescent (cs.wordProd word) s

Membership in the bilinear-inversion set implies a right descent.

theorem DescentInversionBridge.wordSigma_ne_zero {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) : CoxeterGroup.wordSigma M word (CoxeterGroup.e s) ≠ 0

The action of any word on a basis vector $e_s$ is nonzero.

theorem DescentInversionBridge.isNegative_exists_neg_component {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) (hneg : CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e s))) : ∃ (t : B), CoxeterGroup.wordSigma M word (CoxeterGroup.e s) t < 0

A negative root has a strictly negative component.

theorem DescentInversionBridge.descent_exists_neg_component {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.IsRightDescent (cs.wordProd word) s) : ∃ (t : B), CoxeterGroup.wordSigma M word (CoxeterGroup.e s) t < 0

For a reduced word and a right descent $s$, the action on $e_s$ has a strictly negative component.

theorem DescentInversionBridge.ascent_exists_pos_component {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.IsRightDescent (cs.wordProd word) s) : ∃ (t : B), CoxeterGroup.wordSigma M word (CoxeterGroup.e s) t > 0

For a reduced word and a right ascent at $s$, the action on $e_s$ has a strictly positive component.

theorem DescentInversionBridge.bilinInversions_eq_of_wordProd_eq {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word₁ word₂ : List B) (h : cs.wordProd word₁ = cs.wordProd word₂) : CoxeterGroup.bilinInversions M word₁ = CoxeterGroup.bilinInversions M word₂

The bilinear-inversion set depends only on the group element, not on the chosen reduced expression.

theorem DescentInversionBridge.bilinInversions_self_toggle_of_ne_zero {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) (hne : CoxeterGroup.wordSigma M word (CoxeterGroup.e s) s ≠ 0) : s ∈ CoxeterGroup.bilinInversions M (word ++ [s]) ↔ s ∉ CoxeterGroup.bilinInversions M word

Self-toggle for bilinear inversions: when the $s$-component is nonzero, membership of $s$ in $\mathtt{bilinInversions}(\omega s)$ is the negation of membership in $\mathtt{bilinInversions}(\omega)$.

theorem DescentInversionBridge.bilinInversions_nil' {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : CoxeterGroup.bilinInversions M [] = ∅

The bilinear-inversion set of the empty word is empty.

theorem DescentInversionBridge.bilinInversions_singleton' {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : CoxeterGroup.bilinInversions M [s] = {s}

The bilinear-inversion set of a singleton word $[s]$ is $\{s\}$.

theorem DescentInversionBridge.isRightDescent_of_reduced_append {B : Type u_1} {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word : List B) (s : B) (hred : cs.IsReduced (word ++ [s])) : cs.IsRightDescent (cs.wordProd (word ++ [s])) s

If $\omega \cdot s$ is reduced, then $s$ is a right descent of $\omega \cdot s$.

theorem DescentInversionBridge.not_isRightDescent_of_reduced_prefix {B : Type u_1} {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) (word : List B) (s : B) (hred : cs.IsReduced (word ++ [s])) : ¬cs.IsRightDescent (cs.wordProd word) s

If $\omega \cdot s$ is reduced, then $s$ is not a right descent of $\omega$ (otherwise $\omega \cdot s$ would have length $< |\omega| + 1$).