theorem CoxeterGroup.sigma_comp_add {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (v₁ v₂ : B → ℝ) : sigma M s (sigma M t (v₁ + v₂)) = sigma M s (sigma M t v₁) + sigma M s (sigma M t v₂)

The composition $\sigma_s \sigma_t$ is additive.

theorem CoxeterGroup.sigma_comp_smul {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (c : ℝ) (v : B → ℝ) : sigma M s (sigma M t (c • v)) = c • sigma M s (sigma M t v)

The composition $\sigma_s \sigma_t$ commutes with scalar multiplication.

theorem CoxeterGroup.iterate_sigma_comp_add {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (n : ℕ) (v₁ v₂ : B → ℝ) : (fun (w : B → ℝ) => sigma M s (sigma M t w))^[n] (v₁ + v₂) = (fun (w : B → ℝ) => sigma M s (sigma M t w))^[n] v₁ + (fun (w : B → ℝ) => sigma M s (sigma M t w))^[n] v₂

The $n$-fold iterate of $\sigma_s \sigma_t$ is additive.

theorem CoxeterGroup.iterate_sigma_comp_smul {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (n : ℕ) (c : ℝ) (v : B → ℝ) : (fun (w : B → ℝ) => sigma M s (sigma M t w))^[n] (c • v) = c • (fun (w : B → ℝ) => sigma M s (sigma M t w))^[n] v

The $n$-fold iterate of $\sigma_s \sigma_t$ commutes with scalar multiplication.

theorem CoxeterGroup.iterate_sigma_comp_fixes_orthogonal {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (n : ℕ) (w : B → ℝ) (hs : bilinForm M w (e s) = 0) (ht : bilinForm M w (e t) = 0) : (fun (v : B → ℝ) => sigma M s (sigma M t v))^[n] w = w

The $n$-fold iterate of $\sigma_s \sigma_t$ fixes any vector orthogonal to both $e_s$ and $e_t$.

theorem CoxeterGroup.sin_chebyshev_step (θ x : ℝ) : 2 * Real.cos (2 * θ) * Real.sin x - Real.sin (x - 2 * θ) = Real.sin (x + 2 * θ)

Trigonometric step identity used to recognise the Chebyshev recurrence: $2\cos(2\theta)\sin x - \sin(x - 2\theta) = \sin(x + 2\theta)$.

noncomputable def CoxeterGroup.seqA (c α : ℝ) : ℕ → ℝ

The Chebyshev-like sequence $A_n$ that tracks the $e_s$-coefficient of $(\sigma_s \sigma_t)^n (e_s)$ in the geometric representation.

noncomputable def CoxeterGroup.seqB (c α : ℝ) : ℕ → ℝ

The sequence $B_n$ that tracks the $e_t$-coefficient of $(\sigma_s \sigma_t)^n (e_s)$.

noncomputable def CoxeterGroup.seqC (c α : ℝ) : ℕ → ℝ

The sequence $C_n$ that tracks the $e_s$-coefficient of $(\sigma_s \sigma_t)^n (e_t)$.

noncomputable def CoxeterGroup.seqD (c α : ℝ) : ℕ → ℝ

The sequence $D_n$ that tracks the $e_t$-coefficient of $(\sigma_s \sigma_t)^n (e_t)$.

theorem CoxeterGroup.seqC_eq_neg_seqB (c α : ℝ) (n : ℕ) : seqC c α n = -seqB c α n

The sequences $C_n$ and $B_n$ are negatives of each other: $C_n = -B_n$ for all $n$.

theorem CoxeterGroup.seqAB_step (c : ℝ) (n : ℕ) : seqA c (4 * c ^ 2 - 2) (n + 1) = (4 * c ^ 2 - 1) * seqA c (4 * c ^ 2 - 2) n + 2 * c * seqB c (4 * c ^ 2 - 2) n ∧ seqB c (4 * c ^ 2 - 2) (n + 1) = -2 * c * seqA c (4 * c ^ 2 - 2) n - seqB c (4 * c ^ 2 - 2) n

One-step recurrence for the pair $(A_n, B_n)$ giving the matrix product that corresponds to applying one more copy of $\sigma_s \sigma_t$.

theorem CoxeterGroup.seqCD_step (c : ℝ) (n : ℕ) : seqC c (4 * c ^ 2 - 2) (n + 1) = (4 * c ^ 2 - 1) * seqC c (4 * c ^ 2 - 2) n + 2 * c * seqD c (4 * c ^ 2 - 2) n ∧ seqD c (4 * c ^ 2 - 2) (n + 1) = -2 * c * seqC c (4 * c ^ 2 - 2) n - seqD c (4 * c ^ 2 - 2) n

One-step recurrence for the pair $(C_n, D_n)$, analogous to $\mathtt{seqAB\_step}$.

theorem CoxeterGroup.seqA_sin (c α θ : ℝ) (hc : c = -Real.cos θ) (hα : α = 4 * c ^ 2 - 2) (n : ℕ) : Real.sin θ * seqA c α n = Real.sin ((2 * ↑n + 1) * θ)

Closed form for $A_n$ in terms of sines: $\sin\theta \cdot A_n = \sin((2n+1)\theta)$ when $c = -\cos\theta$.

theorem CoxeterGroup.seqB_sin (c α θ : ℝ) (hc : c = -Real.cos θ) (hα : α = 4 * c ^ 2 - 2) (n : ℕ) : Real.sin θ * seqB c α n = Real.sin (2 * ↑n * θ)

Closed form for $B_n$ in terms of sines: $\sin\theta \cdot B_n = \sin(2n\theta)$ when $c = -\cos\theta$.

theorem CoxeterGroup.seqD_sin (c α θ : ℝ) (hc : c = -Real.cos θ) (hα : α = 4 * c ^ 2 - 2) (n : ℕ) : Real.sin θ * seqD c α n = -Real.sin ((2 * ↑n - 1) * θ)

Closed form for $D_n$ in terms of sines: $\sin\theta \cdot D_n = -\sin((2n-1)\theta)$ when $c = -\cos\theta$.

theorem CoxeterGroup.iter_e_s_formula_fn {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (n : ℕ) : (fun (w : B → ℝ) => sigma M s (sigma M t w))^[n] (e s) = seqA (formVal M s t) (4 * formVal M s t ^ 2 - 2) n • e s + seqB (formVal M s t) (4 * formVal M s t ^ 2 - 2) n • e t

Functional form: the $n$-th iterate of $\sigma_s \sigma_t$ applied to $e_s$ is the linear combination $A_n\, e_s + B_n\, e_t$.

theorem CoxeterGroup.iter_e_s_formula {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (n : ℕ) (u : B) : have c := formVal M s t; have α := 4 * c ^ 2 - 2; (fun (w : B → ℝ) => sigma M s (sigma M t w))^[n] (e s) u = seqA c α n * e s u + seqB c α n * e t u

Pointwise form of $\mathtt{iter\_e\_s\_formula\_fn}$: evaluating at any index $u$ gives $A_n\, e_s(u) + B_n\, e_t(u)$.

theorem CoxeterGroup.iter_e_t_formula_fn {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (n : ℕ) : (fun (w : B → ℝ) => sigma M s (sigma M t w))^[n] (e t) = seqC (formVal M s t) (4 * formVal M s t ^ 2 - 2) n • e s + seqD (formVal M s t) (4 * formVal M s t ^ 2 - 2) n • e t

Functional form: the $n$-th iterate of $\sigma_s \sigma_t$ applied to $e_t$ is the linear combination $C_n\, e_s + D_n\, e_t$.

theorem CoxeterGroup.iter_e_t_formula {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) (n : ℕ) (u : B) : have c := formVal M s t; have α := 4 * c ^ 2 - 2; (fun (w : B → ℝ) => sigma M s (sigma M t w))^[n] (e t) u = seqC c α n * e s u + seqD c α n * e t u

Pointwise form of $\mathtt{iter\_e\_t\_formula\_fn}$: evaluating at any index $u$ gives $C_n\, e_s(u) + D_n\, e_t(u)$.

theorem CoxeterGroup.m_ge_two {B : Type u_1} (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : 2 ≤ M.M s t

If $s \ne t$ and the Coxeter order $m(s,t)$ is finite, then $m(s,t) \ge 2$.

theorem CoxeterGroup.sin_theta_pos {B : Type u_1} (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : 0 < Real.sin (Real.pi / ↑(M.M s t))

For $s \ne t$ and finite $m(s,t)$, the angle $\theta = \pi/m(s,t)$ lies strictly between $0$ and $\pi$, so $\sin\theta > 0$.

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

When $m(s,t)$ is finite, the matrix entry $B_{s,t}$ equals $-\cos(\pi/m(s,t))$.

theorem CoxeterGroup.seqA_at_m {B : Type u_1} (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : seqA (formVal M s t) (4 * formVal M s t ^ 2 - 2) (M.M s t) = 1

Endpoint value: $A_{m(s,t)} = 1$, encoding that the $e_s$-coefficient of $(\sigma_s\sigma_t)^{m(s,t)}(e_s)$ returns to $1$.

theorem CoxeterGroup.seqB_at_m {B : Type u_1} (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : seqB (formVal M s t) (4 * formVal M s t ^ 2 - 2) (M.M s t) = 0

Endpoint value: $B_{m(s,t)} = 0$, encoding that the $e_t$-coefficient of $(\sigma_s\sigma_t)^{m(s,t)}(e_s)$ vanishes.

theorem CoxeterGroup.seqC_at_m {B : Type u_1} (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : seqC (formVal M s t) (4 * formVal M s t ^ 2 - 2) (M.M s t) = 0

Endpoint value: $C_{m(s,t)} = 0$, following from $C_n = -B_n$.

theorem CoxeterGroup.seqD_at_m {B : Type u_1} (M : CoxeterMatrix B) (s t : B) (hst : s ≠ t) (hm : M.M s t ≠ 0) : seqD (formVal M s t) (4 * formVal M s t ^ 2 - 2) (M.M s t) = 1

Endpoint value: $D_{m(s,t)} = 1$, encoding that the $e_t$-coefficient of $(\sigma_s\sigma_t)^{m(s,t)}(e_t)$ returns to $1$.