noncomputable def CoxeterGroup.formVal {B : Type u_1} (M : CoxeterMatrix B) (s t : B) : ℝ

Entry $B_{s,t}$ of the bilinear form on the geometric representation.

theorem CoxeterGroup.formVal_symm {B : Type u_1} (M : CoxeterMatrix B) (s t : B) : formVal M s t = formVal M t s

Symmetry: $B_{s,t} = B_{t,s}$.

theorem CoxeterGroup.formVal_diag {B : Type u_1} (M : CoxeterMatrix B) (s : B) : formVal M s s = 1

Diagonal value: $B_{s,s} = 1$.

noncomputable def CoxeterGroup.bilinForm {B : Type u_1} [Fintype B] (M : CoxeterMatrix B) (v w : B → ℝ) : ℝ

The bilinear form on $\mathbb{R}^B$ associated to the Coxeter matrix $M$, defined by $B(v, w) = \sum_{s,t} v_s\, B_{s,t}\, w_t$ where $B_{s,t} = \mathtt{formVal}\,M\,s\,t$. This is the standard form making the geometric representation orthogonal.

noncomputable def CoxeterGroup.e {B : Type u_1} [DecidableEq B] (s : B) : B → ℝ

The standard basis vector $e_s \in \mathbb{R}^B$ supported at $s$ with value $1$.

theorem CoxeterGroup.bilinForm_e_e {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s t : B) : bilinForm M (e s) (e t) = formVal M s t

Evaluating the bilinear form on basis vectors recovers the matrix entry: $B(e_s, e_t) = B_{s,t}$.

noncomputable def CoxeterGroup.sigma {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (v : B → ℝ) : B → ℝ

The reflection $\sigma_s$ on $\mathbb{R}^B$ associated to a simple generator $s$: $\sigma_s(v) = v - 2\, B(v, e_s)\, e_s$. This is the simple reflection in the geometric representation.

theorem CoxeterGroup.sigma_e_self {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : sigma M s (e s) = fun (t : B) => -e s t

The reflection $\sigma_s$ negates $e_s$: $\sigma_s(e_s) = -e_s$.