theorem CoxeterGroup.sigma_support_two {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (r : B) (hr : r = s ∨ r = t) (v : B → ℝ) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) (u : B) : u ≠ s → u ≠ t → sigma M r v u = 0

Support stability for $\sigma_r$ along $\{s, t\}$: if $r \in \{s, t\}$ and $v$ is supported in $\{s, t\}$, then $\sigma_r(v)$ is also supported in $\{s, t\}$.

theorem CoxeterGroup.wordSigma_support_two {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (word : List B) (halt : ∀ b ∈ word, b = s ∨ b = t) (v : B → ℝ) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) (u : B) : u ≠ s → u ≠ t → wordSigma M word v u = 0

Iterated version of $\mathtt{sigma\_support\_two}$: support in $\{s, t\}$ is preserved under $\mathtt{wordSigma}$ for any word in the alphabet $\{s, t\}$.

theorem CoxeterGroup.e_supported_two {B : Type u_1} [DecidableEq B] [Fintype B] (s t u : B) : u ≠ s → u ≠ t → e s u = 0

The simple root $e_s$ is supported in $\{s, t\}$ (vacuously on coordinates outside this pair).

theorem CoxeterGroup.sigma_t_pos_of_t_zero {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (v : B → ℝ) (hpos : IsPositive v) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) (hvt : v t = 0) : IsPositive (sigma M t v)

If $v$ is a positive root supported in $\{s, t\}$ with $v_t = 0$, then $\sigma_t(v)$ is still positive (the $t$-coefficient becomes $-2 v_s\, B_{s,t} \ge 0$).

theorem CoxeterGroup.sigma_s_pos_of_s_zero {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (v : B → ℝ) (hpos : IsPositive v) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) (hvs : v s = 0) : IsPositive (sigma M s v)

Symmetric statement to $\mathtt{sigma\_t\_pos\_of\_t\_zero}$: if $v_s = 0$, then $\sigma_s(v)$ remains positive.

theorem CoxeterGroup.formVal_le_neg_half {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 2) : formVal M s t ≤ -1 / 2

For off-diagonal $s \ne t$ with $m(s, t) \ne 2$ (so $m(s, t) \ge 3$ or $\infty$), the form value satisfies $\mathtt{formVal}\,M\,s\,t \le -1/2$, since $\cos(\pi/3) = 1/2$.

theorem CoxeterGroup.dihedral_pos_len2 {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 2) : IsPositive (wordSigma M [s, t] (e s))

Positivity at length two: when $m(s, t) \ne 2$, $\mathtt{wordSigma}\,M\,[s, t]\,(e_s)$ is still a positive root.

theorem CoxeterGroup.bilinForm_e_t_of_supported {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (v : B → ℝ) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) : bilinForm M v (e t) = v s * formVal M s t + v t

Closed form for $B(v, e_t)$ when $v$ is supported in $\{s, t\}$: $B(v, e_t) = v_s\, B_{s, t} + v_t$.

theorem CoxeterGroup.bilinForm_e_s_of_supported {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (v : B → ℝ) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) : bilinForm M v (e s) = v s + v t * formVal M t s

Closed form for $B(v, e_s)$ when $v$ is supported in $\{s, t\}$: $B(v, e_s) = v_s + v_t\, B_{t, s}$.

theorem CoxeterGroup.sigma_t_coord_t_of_supported {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (v : B → ℝ) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) : sigma M t v t = -v t - 2 * v s * formVal M s t

$t$-coordinate of $\sigma_t(v)$ when $v$ is supported in $\{s, t\}$: $(\sigma_t v)_t = -v_t - 2 v_s\, B_{s, t}$.

theorem CoxeterGroup.sigma_s_coord_s_of_supported {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (v : B → ℝ) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) : sigma M s v s = -v s - 2 * v t * formVal M t s

$s$-coordinate of $\sigma_s(v)$ when $v$ is supported in $\{s, t\}$: $(\sigma_s v)_s = -v_s - 2 v_t\, B_{t, s}$.

theorem CoxeterGroup.sigma_t_pos_general {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (v : B → ℝ) (hpos : IsPositive v) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) (hineq : v t ≤ -2 * v s * formVal M s t) : IsPositive (sigma M t v)

General positivity criterion for $\sigma_t(v)$: a positive root supported in $\{s, t\}$ remains positive under $\sigma_t$ provided $v_t \le -2 v_s\, B_{s, t}$.

theorem CoxeterGroup.sigma_s_pos_general {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (v : B → ℝ) (hpos : IsPositive v) (hsupp : ∀ (u : B), u ≠ s → u ≠ t → v u = 0) (hineq : v s ≤ -2 * v t * formVal M t s) : IsPositive (sigma M s v)

General positivity criterion for $\sigma_s(v)$ symmetric to the previous lemma: a positive root supported in $\{s, t\}$ remains positive under $\sigma_s$ when $v_s \le -2 v_t\, B_{t, s}$.

theorem CoxeterGroup.formVal_eq_neg_one_of_zero {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hm : M.M s t = 0) : formVal M s t = -1

Infinite-order convention: if $m(s, t) = 0$ (interpreted as $\infty$), then $\mathtt{formVal}\,M\,s\,t = -1$.

def CoxeterGroup.altWordEven {B : Type u_1} (s t : B) : ℕ → List B

Even-length alternating word $s\,t\,s\,t\,\cdots$ of length $2n$ starting with $s$, defined recursively.

theorem CoxeterGroup.altWordEven_mem {B : Type u_1} [DecidableEq B] [Fintype B] (s t : B) (n : ℕ) (b : B) : b ∈ altWordEven s t n → b = s ∨ b = t

Every letter of $\mathtt{altWordEven}\,s\,t\,n$ is either $s$ or $t$.

theorem CoxeterGroup.altWordEven_length {B : Type u_1} [DecidableEq B] [Fintype B] (s t : B) (n : ℕ) : (altWordEven s t n).length = 2 * n

$\mathtt{altWordEven}\,s\,t\,n$ has length exactly $2n$.

theorem CoxeterGroup.dihedral_coords_even_infinite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t = 0) (n : ℕ) : wordSigma M (altWordEven s t n) (e s) s = 1 + 2 * ↑n ∧ wordSigma M (altWordEven s t n) (e s) t = 2 * ↑n

Affine (infinite-order) closed forms for the dihedral iterate of $e_s$ along an even-length alternating word: the $s$-coordinate is $1 + 2n$ and the $t$-coordinate is $2n$, reflecting the unipotent action when $m(s, t) = \infty$.

theorem CoxeterGroup.dihedral_coords_odd_infinite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t = 0) (n : ℕ) : wordSigma M (t :: altWordEven s t n) (e s) s = 1 + 2 * ↑n ∧ wordSigma M (t :: altWordEven s t n) (e s) t = 2 * ↑n + 2

Odd-length analogue for $m(s, t) = \infty$: the $s$-coordinate stays $1 + 2n$ while the $t$-coordinate becomes $2n + 2$.

theorem CoxeterGroup.dihedral_pos_even_infinite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t = 0) (n : ℕ) : IsPositive (wordSigma M (altWordEven s t n) (e s))

In the infinite-order case $m(s, t) = 0$, the even-length alternating iterate of $e_s$ is unconditionally positive.

theorem CoxeterGroup.dihedral_pos_odd_infinite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t = 0) (n : ℕ) : IsPositive (wordSigma M (t :: altWordEven s t n) (e s))

Odd-length analogue: in the infinite-order case the iterate $\mathtt{wordSigma}\,M\,(t :: \text{altWord})\,(e_s)$ is also unconditionally positive.

theorem CoxeterGroup.formVal_le_neg_sqrt2_div2 {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (_hst : s ≠ t) (hm : M.M s t = 0 ∨ M.M s t ≥ 4) : formVal M s t ≤ -(√2 / 2)

Sharper bound on the form value: if $m(s, t)$ is either $\infty$ or $\ge 4$, then $\mathtt{formVal}\,M\,s\,t \le -\sqrt{2}/2$, the value $-\cos(\pi/4)$.