noncomputable def TitsCone.pairing {B : Type u_1} [Fintype B] (α x : B → ℝ) : ℝ

def TitsCone.nonposRoots {B : Type u_1} [Fintype B] (Φpos : Set (B → ℝ)) (x : B → ℝ) : Set (B → ℝ)

def TitsCone.nuFiniteAt {B : Type u_1} [Fintype B] (Φpos : Set (B → ℝ)) (x : B → ℝ) : Prop

noncomputable def TitsCone.sigmaWord {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (α : B → ℝ) : B → ℝ

noncomputable def TitsCone.dualSigmaWord {B : Type u_1} (M : CoxeterMatrix B) (ws : List B) (x : B → ℝ) : B → ℝ

class TitsCone.RootSystemData {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Type u_1

• Φpos : Set (B → ℝ)
• roots_in_subspan_finite (I : Finset B) : I ≠ Finset.univ → {α : B → ℝ | α ∈ Φpos M ∧ ∀ s ∉ I, α s = 0}.Finite
• pos_pairing_outside_span (I : Finset B) (x : B → ℝ) : x ∈ titsFaceDual M I → ∀ α ∈ Φpos M, (∃ s ∉ I, α s ≠ 0) → pairing α x > 0
• pairing_word_comm (ws : List B) (α x : B → ℝ) : pairing α (dualSigmaWord M ws x) = pairing (sigmaWord M ws.reverse α) x
• sigmaWord_injective (ws : List B) : Function.Injective (sigmaWord M ws)
• inversions_finite (ws : List B) : {α : B → ℝ | α ∈ Φpos M ∧ sigmaWord M ws α ∉ Φpos M}.Finite
• simple_inversion (s : B) : {α : B → ℝ | α ∈ Φpos M ∧ sigmaWord M [s] α ∉ Φpos M} = {CoxeterGroup.e s}
• nonposRoots_finite_on_hyperplane (v₀ : B → ℝ) : (∀ (s : B), v₀ s > 0) → (∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) → ∀ (x : B → ℝ), ∑ s : B, v₀ s * x s = 1 → (nonposRoots (Φpos M) x).Finite

theorem TitsCone.sigma_involutive {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (v : B → ℝ) : CoxeterGroup.sigma M s (CoxeterGroup.sigma M s v) = v

theorem TitsCone.sigma_injective {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : Function.Injective (CoxeterGroup.sigma M s)

theorem TitsCone.sigmaWord_cons {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (ws' : List B) (α : B → ℝ) : sigmaWord M (s :: ws') α = sigmaWord M ws' (CoxeterGroup.sigma M s α)

theorem TitsCone.sigmaWord_injective_lemma {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) : Function.Injective (sigmaWord M ws)

theorem TitsCone.pairing_dualSigma_eq_sigma_pairing {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (α x : B → ℝ) : pairing α (dualSigma M s x) = pairing (CoxeterGroup.sigma M s α) x

theorem TitsCone.dualSigmaWord_cons {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (ws' : List B) (x : B → ℝ) : dualSigmaWord M (s :: ws') x = dualSigmaWord M ws' (dualSigma M s x)

theorem TitsCone.pairing_word_comm_lemma {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (α x : B → ℝ) : pairing α (dualSigmaWord M ws x) = pairing (sigmaWord M ws.reverse α) x

noncomputable def TitsCone.standardΦpos {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) : Set (B → ℝ)

theorem TitsCone.sigmaWord_eq_wordSigma_reverse {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (v : B → ℝ) : sigmaWord M ws v = CoxeterGroup.wordSigma M ws.reverse v

Translation between the two word-action conventions: $\sigma_w = \text{wordSigma}(w^R)$ where $w^R$ is the reversed word.

theorem TitsCone.sigma_preserves_pos {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) (α : B → ℝ) (hα : α ∈ standardΦpos M) (hne : α ≠ CoxeterGroup.e s) : CoxeterGroup.sigma M s α ∈ standardΦpos M

A positive root $\alpha \neq e_s$ stays in $\Phi^+$ after applying $\sigma_s$. The exception (the simple root $e_s$ itself) becomes $-e_s$, a negative root.

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

Two abstract finiteness hypotheses that supply the standard $\Phi^+$ with a RootSystemData structure: $(1)$ finiteness of roots supported on a proper subset, and $(2)$ finiteness of nonposRoots on the radical hyperplane.

• finiteRoots_in_subspan_of_subset_finite (I : Finset B) : I ≠ Finset.univ → {α : B → ℝ | α ∈ standardΦpos M ∧ ∀ s ∉ I, α s = 0}.Finite
• hyperplane_nonposRoots_finite (v₀ : B → ℝ) : (∀ (s : B), v₀ s > 0) → (∀ (t : B), ∑ u : B, v₀ u * CoxeterGroup.formVal M u t = 0) → ∀ (x : B → ℝ), ∑ s : B, v₀ s * x s = 1 → (nonposRoots (standardΦpos M) x).Finite

theorem TitsCone.sigmaWord_append_singleton {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (s : B) (α : B → ℝ) : sigmaWord M (ws ++ [s]) α = CoxeterGroup.sigma M s (sigmaWord M ws α)

Appending one letter: $\sigma_{w \cdot s}(\alpha) = \sigma_s(\sigma_w(\alpha))$.

theorem TitsCone.inversions_append_finite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) (s : B) (ih : {α : B → ℝ | α ∈ standardΦpos M ∧ sigmaWord M ws α ∉ standardΦpos M}.Finite) : {α : B → ℝ | α ∈ standardΦpos M ∧ sigmaWord M (ws ++ [s]) α ∉ standardΦpos M}.Finite

Inductive step for the finiteness of inversion sets: if the inversion set of $w$ is finite, so is the inversion set of $w \cdot s$.

theorem TitsCone.e_mem_inversion_singleton {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : CoxeterGroup.e s ∈ standardΦpos M ∧ sigmaWord M [s] (CoxeterGroup.e s) ∉ standardΦpos M

The simple root $e_s$ is positive but $\sigma_s(e_s) = -e_s$ is not in $\Phi^+$: the unique inversion of the simple reflection $s$ is $e_s$.

noncomputable def TitsCone.rootSystemData_standard {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hfpp : FiniteProperParabolicsHyp M) : RootSystemData M

Construction of RootSystemData from the standard positive roots, given the two finiteness hypotheses encapsulated in FiniteProperParabolicsHyp.

theorem TitsCone.face_subset_nuFinite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [RootSystemData M] (I : Finset B) (hI : I ≠ Finset.univ) (x : B → ℝ) (hx : x ∈ titsFaceDual M I) : nuFiniteAt (RootSystemData.Φpos M) x

Every point of a proper face $F_I$ (with $I \neq \emptyset$, i.e. $I \neq$ all simple roots) has nu-finiteness: only finitely many positive roots pair nonpositively.

theorem TitsCone.wAction_face_nuFinite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [RootSystemData M] (ws : List B) (I : Finset B) (hI : I ≠ Finset.univ) (y : B → ℝ) (hy : y ∈ titsFaceDual M I) : nuFiniteAt (RootSystemData.Φpos M) (dualSigmaWord M ws y)

The $W$-translate $w \cdot F_I$ of a proper Tits face is nu-finite at every point. This bounds the nonposRoots set by inversions plus translated face-finiteness.

theorem TitsCone.dualSigmaWord_eq_wordAction {B : Type u_1} [DecidableEq B] [Fintype B] {M : CoxeterMatrix B} (ws : List B) (x : B → ℝ) : dualSigmaWord M ws x = wordAction M ws x

dualSigmaWord and wordAction are definitionally equal: both fold $\sigma^\vee_s$ left-to-right along the word.

theorem TitsCone.dualSigma_zero {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (s : B) : dualSigma M s 0 = 0

The dual simple reflection fixes the origin: $\sigma^\vee_s(0) = 0$.

theorem TitsCone.wordAction_zero {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (ws : List B) : wordAction M ws 0 = 0

Any word fixes the origin: $w \cdot 0 = 0$.

theorem TitsCone.closure_mem_zero_or_face {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (y : B → ℝ) (hy : y ∈ titsFundamentalClosure M) : y = 0 ∨ ∃ (I : Finset B), I ≠ Finset.univ ∧ y ∈ titsFaceDual M I

Each point of the fundamental closure is either the origin or lies in some proper face $F_I$ with $I$ the set of vanishing coordinates.

theorem TitsCone.titsCone_face_decomp {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (x : B → ℝ) (hx : x ∈ titsConeSet M) : x = 0 ∨ ∃ (I : Finset B) (ws : List B) (y : B → ℝ), I ≠ Finset.univ ∧ y ∈ titsFaceDual M I ∧ x = dualSigmaWord M ws y

Face decomposition of the Tits cone: every $x \in U$ is either zero or lies in the $W$-translate of a proper Tits face $F_I$.

theorem TitsCone.pairing_e {B : Type u_1} [DecidableEq B] [Fintype B] (s : B) (x : B → ℝ) : pairing (CoxeterGroup.e s) x = x s

Evaluation at the standard basis vector $e_s$: $\langle e_s, x\rangle = x_s$.

theorem TitsCone.sigmaWord_singleton {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [RootSystemData M] (s : B) (α : B → ℝ) : sigmaWord M [s] α = CoxeterGroup.sigma M s α

Singleton word: $\sigma_{[s]} = \sigma_s$.

theorem TitsCone.pairing_neg {B : Type u_1} [DecidableEq B] [Fintype B] (α x : B → ℝ) : pairing (fun (t : B) => -α t) x = -pairing α x

Negation in the first argument: $\langle-\alpha, x\rangle = -\langle\alpha, x\rangle$.

theorem TitsCone.pairing_e_dualSigma {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [RootSystemData M] (s : B) (y : B → ℝ) : pairing (CoxeterGroup.e s) (dualSigma M s y) = -y s

Sign-flip identity: $\langle e_s, \sigma^\vee_s y\rangle = -y_s$.

theorem TitsCone.e_mem_nonposRoots_of_neg {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [RootSystemData M] [RootSystemData M] (s : B) (y : B → ℝ) (hs : y s < 0) (he_mem : CoxeterGroup.e s ∈ RootSystemData.Φpos M) : CoxeterGroup.e s ∈ nonposRoots (RootSystemData.Φpos M) y

If $y_s < 0$ and $e_s \in \Phi^+$, then $e_s$ belongs to the set of positive roots with nonpositive pairing at $y$.

theorem TitsCone.e_not_in_sigmaWord_image {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [RootSystemData M] [RootSystemData M] (s : B) (y : B → ℝ) (hs : y s < 0) : CoxeterGroup.e s ∉ sigmaWord M [s] '' nonposRoots (RootSystemData.Φpos M) (dualSigma M s y)

The simple root $e_s$ is not in the image of $\sigma_s$ on the nonposRoots of $\sigma^\vee_s y$, used to obtain a strict cardinality drop in the induction.

theorem TitsCone.nuFinite_mem_titsCone {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [RootSystemData M] (x : B → ℝ) (_hx : x ≠ 0) (hnu : nuFiniteAt (RootSystemData.Φpos M) x) : x ∈ titsConeSet M

Converse direction of the Tits cone characterisation: any $x \neq 0$ satisfying nu-finiteness lies in $U$. The proof inducts on the cardinality of the nonposRoots set, using a simple reflection at a negative coordinate to strictly shrink it.

theorem TitsCone.titsCone_eq_zero_union_nuFinite {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) [RootSystemData M] : titsConeSet M = {x : B → ℝ | x = 0} ∪ {x : B → ℝ | nuFiniteAt (RootSystemData.Φpos M) x}

Main characterisation of the Tits cone: $U = \{0\} \cup \{x : \text{nu-finite at } x\}$. A point lies in $U$ iff it is zero or only finitely many positive roots are nonpositive on it.