def TitsCone.coxeterWall {B : Type u_1} (_M : CoxeterMatrix B) (s : B) : Set (B → ℝ)

The Coxeter wall $H_s = \{\varphi : \varphi_s = 0\}$ associated to a simple reflection $s$.

def TitsCone.coxeterUpperHalf {B : Type u_1} (_M : CoxeterMatrix B) (s : B) : Set (B → ℝ)

The positive half-space $H_s^+ = \{\varphi : \varphi_s > 0\}$ cut out by the wall $H_s$.

def TitsCone.coxeterLowerHalf {B : Type u_1} (_M : CoxeterMatrix B) (s : B) : Set (B → ℝ)

The negative half-space $H_s^- = \{\varphi : \varphi_s < 0\}$ cut out by the wall $H_s$.

def TitsCone.titsFundamentalChamber {B : Type u_1} (_M : CoxeterMatrix B) : Set (B → ℝ)

The open fundamental chamber $C = \bigcap_s H_s^+ = \{\varphi : \forall s, \varphi_s > 0\}$.

def TitsCone.titsFaceDual {B : Type u_1} (_M : CoxeterMatrix B) (I : Finset B) : Set (B → ℝ)

The standard face of type $I \subseteq B$: $F_I = \{\varphi : \varphi_s = 0 \text{ for } s \in I, \ \varphi_s > 0 \text{ for } s \notin I\}$.

noncomputable def TitsCone.dualSigma {B : Type u_1} (M : CoxeterMatrix B) (s : B) (x : B → ℝ) : B → ℝ

The contragredient action of a simple reflection $s$ on coordinates: $\sigma^*_s(x)_t = x_t - 2 x_s \cdot B(\alpha_s, \alpha_t)$.

def TitsCone.titsFundamentalClosure {B : Type u_1} (_M : CoxeterMatrix B) : Set (B → ℝ)

The closed fundamental chamber $\overline{C} = \{\varphi : \forall s, \varphi_s \ge 0\}$.

def TitsCone.titsConeSet {B : Type u_1} (M : CoxeterMatrix B) : Set (B → ℝ)

The Tits cone $\mathcal U = W \cdot \overline{C}$: $W$-orbit of the closed fundamental chamber under the contragredient action.

theorem TitsCone.dualSigma_on_s {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (x : B → ℝ) : dualSigma M s x s = -x s

The dual reflection flips the $s$-coordinate: $\sigma^*_s(x)_s = -x_s$.

theorem TitsCone.titsFundamentalClosure_subset_titsCone {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : titsFundamentalClosure M ⊆ titsConeSet M

$\overline{C} \subseteq \mathcal U$: the closed fundamental chamber is in the Tits cone (realized as the orbit of $\overline{C}$ under the empty word).

theorem TitsCone.dualSigma_involutive {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (x : B → ℝ) : dualSigma M s (dualSigma M s x) = x

The dual action is an involution: $\sigma^*_s \circ \sigma^*_s = \mathrm{id}$.

theorem CoxeterGroup.bilinForm_zero {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : bilinForm M 0 0 = 0

The Coxeter bilinear form vanishes at the origin: $B(0,0) = 0$.

def CoxeterGroup.FormIndecomposable {B : Type u_1} [Fintype B] (f : B → B → ℝ) : Prop

A symmetric matrix $f$ is indecomposable iff no proper subset $\emptyset \ne I \subsetneq B$ is "block-diagonal": every such $I$ has a nonzero off-block entry $f_{ij} \ne 0$ with $i \in I$, $j \notin I$.

theorem CoxeterGroup.IsAffineCoxeterForm {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : (FormIndecomposable fun (s t : B) => formVal M s t) ∧ (∀ (v : B → ℝ), bilinForm M v v ≥ 0) ∧ ¬((∀ (v : B → ℝ), bilinForm M v v ≥ 0) ∧ ∀ (v : B → ℝ), bilinForm M v v = 0 → v = 0) ↔ (FormIndecomposable fun (s t : B) => formVal M s t) ∧ (∀ (v : B → ℝ), bilinForm M v v ≥ 0) ∧ ∃ (v : B → ℝ), v ≠ 0 ∧ bilinForm M v v = 0

Equivalent formulations of "affine Coxeter form": indecomposable + PSD + nondefinite is the same as indecomposable + PSD + degenerate (existence of a nontrivial null vector).

class PerronFrobeniusProperty {B : Type u_2} [Fintype B] (f : B → B → ℝ) : Prop

The Perron–Frobenius property for an indecomposable PSD off-diagonal-nonpositive form: the kernel is 1-dimensional and spanned by a strictly positive vector $v > 0$.

• kernel_span : CoxeterGroup.FormIndecomposable f → (∀ (v : B → ℝ), ∑ s : B, ∑ t : B, v s * f s t * v t ≥ 0) → (∃ (v : B → ℝ), v ≠ 0 ∧ ∑ s : B, ∑ t : B, v s * f s t * v t = 0) → (∀ (s t : B), s ≠ t → f s t ≤ 0) → ∃ (v : B → ℝ), (∀ (s : B), v s > 0) ∧ ∀ (w : B → ℝ), ∑ s : B, ∑ t : B, w s * f s t * w t = 0 → ∃ (c : ℝ), w = fun (b : B) => c * v b

theorem perronFrobenius_kernel_dim_one {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (f : B → B → ℝ) [hPF : PerronFrobeniusProperty f] (hIndecomp : CoxeterGroup.FormIndecomposable f) (hPSD : ∀ (v : B → ℝ), ∑ s : B, ∑ t : B, v s * f s t * v t ≥ 0) (hNotPD : ∃ (v : B → ℝ), v ≠ 0 ∧ ∑ s : B, ∑ t : B, v s * f s t * v t = 0) (hOffDiag : ∀ (s t : B), s ≠ t → f s t ≤ 0) : ∃ (v : B → ℝ), (∀ (s : B), v s > 0) ∧ ∀ (w : B → ℝ), ∑ s : B, ∑ t : B, w s * f s t * w t = 0 → ∃ (c : ℝ), w = fun (b : B) => c * v b

Convenience accessor: under the Perron–Frobenius hypothesis, the kernel of a degenerate indecomposable PSD off-diagonal-nonpositive form is 1-dimensional with strictly positive generator.

theorem perronFrobenius_submatrix_pos_def {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (f : B → B → ℝ) [hPF : PerronFrobeniusProperty f] (hIndecomp : CoxeterGroup.FormIndecomposable f) (hPSD : ∀ (v : B → ℝ), ∑ s : B, ∑ t : B, v s * f s t * v t ≥ 0) (hOffDiag : ∀ (s t : B), s ≠ t → f s t ≤ 0) (b₀ : B) (w : B → ℝ) : w b₀ = 0 → w ≠ 0 → ∑ s : B, ∑ t : B, w s * f s t * w t > 0

Consequence: under PF hypothesis, any nonzero vector $w$ vanishing at a single index $b_0$ satisfies $Q_f(w) > 0$. This is the form-theoretic version of "any proper principal submatrix is PD".

class SphericalFiniteProperty {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Prop

Hypothesis class encoding the Coxeter classification theorem: a positive-definite Coxeter form implies the underlying Coxeter group is finite (spherical type). Used as an axiom locally to avoid invoking the full classification.

• finite_of_pos_def : (∀ (v : B → ℝ), v ≠ 0 → CoxeterGroup.bilinForm M v v > 0) → Finite M.Group

theorem spherical_implies_finite_group {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [hSF : SphericalFiniteProperty M] (h : ∀ (v : B → ℝ), v ≠ 0 → CoxeterGroup.bilinForm M v v > 0) : Finite M.Group

Convenience accessor: positive-definite Coxeter form implies finite Coxeter group.

def CoxeterMatrix.restrict {B : Type u_1} (M : CoxeterMatrix B) (I : Finset B) : CoxeterMatrix ↥I

Restriction of a Coxeter matrix $M$ to the parabolic subset $I \subseteq B$ of generators.

noncomputable def extendByZero {B : Type u_1} [DecidableEq B] (I : Finset B) (v : ↥I → ℝ) : B → ℝ

Extend a vector $v : I \to \mathbb R$ to all of $B \to \mathbb R$ by setting components outside $I$ to zero.

theorem extendByZero_outside {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] {I : Finset B} {b : B} (hb : b ∉ I) (v : ↥I → ℝ) : extendByZero I v b = 0

$\mathrm{extendByZero}(v)$ vanishes outside $I$.

theorem extendByZero_ne_zero {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] {I : Finset B} {v : ↥I → ℝ} (hv : v ≠ 0) : extendByZero I v ≠ 0

$\mathrm{extendByZero}$ is injective on nonzero vectors.

theorem sum_restrict_of_vanish {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (I : Finset B) (f : B → ℝ) (hf : ∀ b ∉ I, f b = 0) : ∑ b : B, f b = ∑ b : ↥I, f ↑b

A sum over $B$ restricts to a sum over $I$ when the summand vanishes outside $I$.

theorem bilinForm_restrict_eq_extend {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (M : CoxeterMatrix B) (I : Finset B) (v : ↥I → ℝ) : CoxeterGroup.bilinForm (M.restrict I) v v = CoxeterGroup.bilinForm M (extendByZero I v) (extendByZero I v)

The restricted Coxeter form on $I$ agrees with the original form on the zero-extension: $B_{M|_I}(v, v) = B_M(\bar v, \bar v)$ where $\bar v$ is $\mathrm{extendByZero}(v)$.

theorem perronFrobenius_proper_subset_pos_def {B : Type u_1} [DecidableEq B] [Fintype B] [Nonempty B] (M : CoxeterMatrix B) [hPF : PerronFrobeniusProperty fun (s t : B) => CoxeterGroup.formVal M s t] (hIndecomp : CoxeterGroup.FormIndecomposable fun (s t : B) => CoxeterGroup.formVal M s t) (hPSD : ∀ (v : B → ℝ), CoxeterGroup.bilinForm M v v ≥ 0) (hOffDiag : ∀ (s t : B), s ≠ t → CoxeterGroup.formVal M s t ≤ 0) (I : Finset B) (hI : I ≠ Finset.univ) (v : ↥I → ℝ) : v ≠ 0 → CoxeterGroup.bilinForm (M.restrict I) v v > 0

Main corollary of Perron–Frobenius for affine Coxeter forms: the form restricted to any proper subset of generators $I \subsetneq B$ is positive definite.

structure GeomRealization.GeomRealizationPoint (V : Type u_2) [Fintype V] : Type u_2

A point of the geometric realization: barycentric weights $\sum_v p_v = 1$, $p_v \ge 0$.

• wt : V → ℝ
• wt_nonneg (v : V) : self.wt v ≥ 0
• wt_sum : ∑ v : V, self.wt v = 1

noncomputable def GeomRealization.geomRealizationDist {V : Type u_1} [Fintype V] [Nonempty V] (p q : GeomRealizationPoint V) : ℝ

$\ell^\infty$ distance between two geometric-realization points.

noncomputable def GeomRealization.vertexPoint {V : Type u_1} [DecidableEq V] [Fintype V] (v : V) : GeomRealizationPoint V

The $\delta_v$-point: vertex $v$ embedded as a geometric realization point.