noncomputable def CoxeterExchangeGenuine.rootSequence {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (s : B) (k : ℕ) : B → ℝ

The root sequence read off from a word $\omega$ and a simple root $e_s$: the $k$-th term is the geometric image of $e_s$ under the suffix of $\omega$ of length $k$. Used to detect sign changes along the word.

structure CoxeterExchangeGenuine.GeometricBridgeHyp {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : Prop

Geometric bridge hypothesis: bundles the two implications connecting the abstract length function and the geometric representation. Field $\mathtt{length\_decrease\_negative}$ says length-decrease on right multiplication implies negativity of the resulting root, and field $\mathtt{sign\_change\_exchange}$ says negativity implies the exchange relation $\omega = \omega' \cdot s$ for some deletion of $\omega$.

• length_decrease_negative (word : List B) (s : B) : cs.IsReduced word → cs.length (cs.wordProd word * cs.simple s) < cs.length (cs.wordProd word) → CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e s))
• sign_change_exchange (word : List B) (s : B) : cs.IsReduced word → CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e s)) → ∃ (i : Fin word.length), cs.wordProd (word.eraseIdx ↑i) = cs.wordProd word * cs.simple s

theorem CoxeterExchangeGenuine.exchange_from_bridge {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} (bridge : GeometricBridgeHyp M cs) : CoxeterExchange.SatisfiesExchangeCondition M cs

Given the geometric bridge hypothesis, the abstract exchange condition follows by composing length-decrease implies negativity with negativity implies exchange.

theorem CoxeterExchangeGenuine.bilinForm_neg_left {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v w : B → ℝ) : CoxeterGroup.bilinForm M (-v) w = -CoxeterGroup.bilinForm M v w

The bilinear form is anti-linear under negation in its first slot: $B(-v, w) = -B(v, w)$.

theorem CoxeterExchangeGenuine.e_self_coord_positive {B : Type u_1} [DecidableEq B] (s : B) : CoxeterGroup.e s s > 0

The simple root $e_s$ has strictly positive $s$-coordinate, namely $1$.

theorem CoxeterExchangeGenuine.exists_sign_change (f : ℕ → ℝ) (n : ℕ) (_hn : 0 < n) (hf0 : f 0 > 0) (hfn : f n < 0) : ∃ k < n, f k ≥ 0 ∧ f (k + 1) < 0

Sign-change lemma: a sequence $f : \mathbb{N} \to \mathbb{R}$ with $f(0) > 0$ and $f(n) < 0$ has some index $k < n$ where $f(k) \ge 0$ but $f(k+1) < 0$.

theorem CoxeterExchangeGenuine.exists_sign_change' (f : ℕ → ℝ) (n : ℕ) (_hn : 0 < n) (hf0 : f 0 > 0) (hfn : f n ≤ 0) : ∃ k < n, f k > 0 ∧ f (k + 1) ≤ 0

Strict-to-non-strict variant of $\mathtt{exists\_sign\_change}$: $f(0) > 0$ and $f(n) \le 0$ give an index $k$ with $f(k) > 0$ and $f(k+1) \le 0$.

structure CoxeterExchangeGenuine.RootSignChangeHyp {B : Type u_1} [DecidableEq B] [Fintype B] {W : Type u_2} [Group W] (M : CoxeterMatrix B) (cs : CoxeterSystem M W) : Prop

A more granular bridge hypothesis: for any reduced word $\omega$ and simple root $e_s$ whose total geometric image is negative, an index $k$ witnessing the sign change of the $s$-coordinate yields an exchange $\omega = \omega' \cdot s$ for some deletion of $\omega$.

• sign_change_at_index (word : List B) (s : B) (k : ℕ) : cs.IsReduced word → k < word.length → CoxeterGroup.IsNegative (CoxeterGroup.wordSigma M word (CoxeterGroup.e s)) → CoxeterGroup.wordSigma M (List.drop (word.length - k) word) (CoxeterGroup.e s) s > 0 → CoxeterGroup.wordSigma M (List.drop (word.length - (k + 1)) word) (CoxeterGroup.e s) s ≤ 0 → ∃ (i : Fin word.length), cs.wordProd (word.eraseIdx ↑i) = cs.wordProd word * cs.simple s