theorem CoxeterGroup.sin_chebyshev_recurrence (θ : ℝ) (n : ℕ) : Real.sin ((↑n + 2) * θ) = 2 * Real.cos θ * Real.sin ((↑n + 1) * θ) - Real.sin (↑n * θ)

Chebyshev-type recurrence for $\sin$: $\sin((n + 2) \theta) = 2 \cos\theta \sin((n + 1)\theta) - \sin(n\theta)$, the standard three-term linear recurrence satisfied by $U_n(\cos\theta) = \sin((n+1)\theta)/\sin\theta$.

theorem CoxeterGroup.formVal_eq_neg_cos {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hm : M.M s t ≠ 0) : formVal M s t = -Real.cos (Real.pi / ↑(M.M s t))

For $m(s, t) \ne 0$ the bilinear form value is the negative cosine $\mathtt{formVal}\,M\,s\,t = -\cos(\pi / m(s, t))$.

theorem CoxeterGroup.dihedral_coords_even_finite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) (k : ℕ) : have θ := Real.pi / ↑(M.M s t); wordSigma M (altWordEven s t k) (e s) s = Real.sin ((2 * ↑k + 1) * θ) / Real.sin θ ∧ wordSigma M (altWordEven s t k) (e s) t = Real.sin (2 * ↑k * θ) / Real.sin θ

Closed-form formulas for the $s$- and $t$-coordinates of the dihedral iterate $\mathtt{wordSigma}$ of $e_s$ along an even-length alternating word when $m(s, t)$ is finite. Both coordinates are ratios of sines built from $\theta = \pi / m(s, t)$.

theorem CoxeterGroup.dihedral_coords_odd_finite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) (k : ℕ) : have θ := Real.pi / ↑(M.M s t); wordSigma M (t :: altWordEven s t k) (e s) s = Real.sin ((2 * ↑k + 1) * θ) / Real.sin θ ∧ wordSigma M (t :: altWordEven s t k) (e s) t = Real.sin ((2 * ↑k + 2) * θ) / Real.sin θ

Odd-length analogue of $\mathtt{dihedral\_coords\_even\_finite}$: closed forms for the coordinates of $\mathtt{wordSigma}\,(t :: \text{altWord})\,(e_s)$ in terms of sines at multiples of $\theta = \pi / m(s, t)$.

theorem CoxeterGroup.sin_nonneg_of_nat_le (m n : ℕ) (hm : m ≠ 0) (hn_le : n ≤ m) : 0 ≤ Real.sin (↑n * (Real.pi / ↑m))

Non-negativity of $\sin(n \pi / m)$ for $0 \le n \le m$, since the argument lies in $[0, \pi]$.

theorem CoxeterGroup.dihedral_pos_even_finite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) (k : ℕ) (hk : 2 * k < M.M s t) : IsPositive (wordSigma M (altWordEven s t k) (e s))

In the finite-order dihedral case ($m(s,t)$ finite), the iterate $\mathtt{wordSigma}\,M\,(\mathtt{altWordEven}\,s\,t\,k)\,(e_s)$ is a positive root as long as $2k < m(s, t)$.

theorem CoxeterGroup.dihedral_pos_odd_finite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) (k : ℕ) (hk : 2 * k + 1 < M.M s t) : IsPositive (wordSigma M (t :: altWordEven s t k) (e s))

Odd-length version of $\mathtt{dihedral\_pos\_even\_finite}$: prepending a $t$ keeps the iterate positive as long as $2k + 1 < m(s, t)$.

theorem CoxeterGroup.dihedral_pos_even {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (k : ℕ) (hk : 2 * k < M.M s t ∨ M.M s t = 0) : IsPositive (wordSigma M (altWordEven s t k) (e s))

Combined dihedral positivity (even length): the alternating iterate of $e_s$ stays positive as long as $2k < m(s, t)$ in the finite case, or unconditionally in the infinite case $m(s, t) = 0$.

theorem CoxeterGroup.dihedral_pos_odd {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (k : ℕ) (hk : 2 * k + 1 < M.M s t ∨ M.M s t = 0) : IsPositive (wordSigma M (t :: altWordEven s t k) (e s))

Combined dihedral positivity (odd length): the alternating iterate $\mathtt{wordSigma}\,M\,(t :: \text{altWord})\,(e_s)$ stays positive provided $2k + 1 < m(s, t)$, with the infinite case $m(s, t) = 0$ unconditional.