theorem TitsCone.pairing_convex_combination_pos {B : Type u_1} [DecidableEq B] [Fintype B] (α y z : B → ℝ) (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hy : pairing α y > 0) (hz : pairing α z > 0) : (pairing α fun (s : B) => (1 - t) * y s + t * z s) > 0

The pairing is linear in the second argument, so if $\langle \alpha, y\rangle > 0$ and $\langle \alpha, z\rangle > 0$ then $\langle \alpha, (1-t)y + tz\rangle > 0$ for any $t \in [0,1]$.

theorem TitsCone.hyperplane_meets_segment_implies_nonpos {B : Type u_1} [DecidableEq B] [Fintype B] (α y z : B → ℝ) (t : ℝ) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (h : (pairing α fun (s : B) => (1 - t) * y s + t * z s) = 0) : pairing α y ≤ 0 ∨ pairing α z ≤ 0

Contrapositive: if a reflecting hyperplane $\{x : \langle\alpha, x\rangle = 0\}$ meets the segment $[y, z]$, then at least one endpoint satisfies $\langle\alpha, \cdot\rangle \le 0$.

theorem TitsCone.segment_meets_finite_roots {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [Nonempty B] [inst : RootSystemData M] (v₀ : B → ℝ) (hv₀_pos : ∀ (s : B), v₀ s > 0) (hv₀_rad : ∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) (y z : B → ℝ) (hy : y ∈ titsConeSet M \ {0}) (hz : z ∈ titsConeSet M \ {0}) : {α : B → ℝ | α ∈ RootSystemData.Φpos M ∧ ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ (pairing α fun (s : B) => (1 - t) * y s + t * z s) = 0}.Finite

Local finiteness: any segment $[y,z] \subset \mathcal U \setminus \{0\}$ meets only finitely many reflecting hyperplanes. The proof bounds these roots by the union of nonposRoots at the two endpoints, both of which are finite.