theorem TitsCone.standardΦpos_form_eq_one {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (α : B → ℝ) (hα : α ∈ standardΦpos M) : CoxeterGroup.bilinForm M α α = 1

Every positive root $\alpha \in \Phi^+$ has unit length for the Coxeter form: $B(\alpha,\alpha) = 1$. This follows from the fact that simple roots have unit length and the form is $W$-invariant.

structure TitsCone.AffineCoxeterHyp {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Prop

Hypotheses isolating the two key properties of an affine, crystallographic Coxeter system used in the proofs: (1) coercivity of the form $B$ on every proper parabolic subspace, and (2) integrality of the coordinates of every positive root in the simple-root basis.

• coercive_on_proper_subset (I : Finset B) : I ≠ Finset.univ → ∃ (c : ℝ), 0 < c ∧ ∀ (v : B → ℝ), (∀ s ∉ I, v s = 0) → c * ∑ b : B, v b ^ 2 ≤ CoxeterGroup.bilinForm M v v
• roots_integer_coords (α : B → ℝ) : α ∈ standardΦpos M → ∀ (b : B), ∃ (n : ℤ), α b = ↑n

theorem TitsCone.finiteRoots_in_subspan_of_AffineCoxeterHyp {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hyp : AffineCoxeterHyp M) (I : Finset B) : I ≠ Finset.univ → {α : B → ℝ | α ∈ standardΦpos M ∧ ∀ s ∉ I, α s = 0}.Finite

Under the affine Coxeter hypothesis, the set of positive roots supported on any proper subset $I \subsetneq B$ of simple reflections is finite. This is the "spherical-on-parabolics" finiteness statement and is what makes proper parabolic subgroups finite.

theorem TitsCone.bilinForm_radical_shift_eq {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (v₀ w : B → ℝ) (a : ℝ) (hrad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) : ∑ s : B, ∑ t : B, (w s - a * v₀ s) * CoxeterGroup.formVal M s t * (w t - a * v₀ t) = ∑ s : B, ∑ t : B, w s * CoxeterGroup.formVal M s t * w t

Shifting by a radical vector does not change the Coxeter form: $B(w - a v_0, w - a v_0) = B(w,w)$ when $v_0 \in \mathrm{rad}(B)$.

theorem TitsCone.norm_sq_le_of_perp_shift {B : Type u_1} [DecidableEq B] [Fintype B] (v₀ w : B → ℝ) (a : ℝ) (hperp : ∑ s : B, v₀ s * w s = 0) : ∑ s : B, w s ^ 2 ≤ ∑ s : B, (w s - a * v₀ s) ^ 2

Pythagoras-style inequality: if $w \perp v_0$ then $\|w\|^2 \le \|w - a v_0\|^2$ for any $a$.

theorem TitsCone.bilinForm_on_v0_perp_coercive {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hyp : AffineCoxeterHyp M) (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_radical : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) : ∃ c_min > 0, ∀ (w : B → ℝ), ∑ s : B, v₀ s * w s = 0 → c_min * ∑ s : B, w s ^ 2 ≤ ∑ s : B, ∑ t : B, w s * CoxeterGroup.formVal M s t * w t

The Coxeter form $B$ is coercive on the hyperplane $v_0^{\perp}$: there exists $c > 0$ with $c \|w\|^2 \le B(w,w)$ for all $w$ with $\langle v_0, w \rangle = 0$. This is the key spectral estimate driving finiteness of nonpositive-roots sets.

theorem TitsCone.abs_inner_le_sqrt_norms {B : Type u_1} [DecidableEq B] [Fintype B] (a b : B → ℝ) {C : ℝ} (hC : 0 ≤ C) (ha : ∑ s : B, a s ^ 2 ≤ C) : |∑ s : B, a s * b s| ≤ √C * √(∑ s : B, b s ^ 2)

Cauchy–Schwarz with a bound: $|\langle a, b\rangle| \le \sqrt C \cdot \|b\|$ when $\|a\|^2 \le C$.

theorem TitsCone.sum_sq_orth_decomp {B : Type u_1} [DecidableEq B] [Fintype B] (v₀ w : B → ℝ) (c : ℝ) (hperp : ∑ s : B, v₀ s * w s = 0) : ∑ s : B, (c * v₀ s + w s) ^ 2 = c ^ 2 * ∑ s : B, v₀ s ^ 2 + ∑ s : B, w s ^ 2

Pythagoras decomposition: $\|c v_0 + w\|^2 = c^2 \|v_0\|^2 + \|w\|^2$ when $w \perp v_0$.

theorem TitsCone.nonposRoots_coord_bound {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hyp : AffineCoxeterHyp M) (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_radical : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (x : B → ℝ) (hx_hyp : ∑ s : B, v₀ s * x s = 1) (hcoercive : ∃ c_min > 0, ∀ (w : B → ℝ), ∑ s : B, v₀ s * w s = 0 → c_min * ∑ s : B, w s ^ 2 ≤ ∑ s : B, ∑ t : B, w s * CoxeterGroup.formVal M s t * w t) : ∃ (C : ℝ), ∀ α ∈ nonposRoots (standardΦpos M) x, ∀ (s : B), α s ≤ C ∧ 0 ≤ α s

Uniform coordinate bound: every root $\alpha \in \Phi^+$ with $\langle \alpha, x\rangle \le 0$ has all coordinates in $[0, C]$ for a constant $C$ depending only on $v_0$, $x$, and the coercivity constant.

theorem TitsCone.hyperplane_nonposRoots_finite_axiom {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hyp : AffineCoxeterHyp M) (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_radical : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (x : B → ℝ) (hx_hyp : ∑ s : B, v₀ s * x s = 1) : (nonposRoots (standardΦpos M) x).Finite

Combining the coordinate bound with integrality: for $x$ on the affine hyperplane, the set of positive roots with $\langle \alpha, x\rangle \le 0$ is finite.

def TitsCone.finiteProperParabolicsHyp_of_affineCoxeterHyp {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hyp : AffineCoxeterHyp M) : FiniteProperParabolicsHyp M

Packaging: from AffineCoxeterHyp we obtain the two finiteness axioms needed by the rest of the development (subspan finiteness and hyperplane finiteness of nonposRoots).