def AffineCoxeterHypProof.IsCrystallographic {B : Type u_1} (M : CoxeterMatrix B) : Prop

A Coxeter matrix is crystallographic if $2 \cos(\pi/m_{st}) \in \mathbb Z$ for all $s,t \in B$, i.e. all entries of the doubled Gram matrix are integers. This is the condition for the associated root system to admit an integral coroot lattice.

theorem AffineCoxeterHypProof.coercive_on_proper_subset_of_affine {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hIndecomp : CoxeterGroup.FormIndecomposable fun (s t : B) => CoxeterGroup.formVal M s t) (hPSD : ∀ (v : B → ℝ), CoxeterGroup.bilinForm M v v ≥ 0) (I : Finset B) (hI : I ≠ Finset.univ) : ∃ (c : ℝ), 0 < c ∧ ∀ (v : B → ℝ), (∀ s ∉ I, v s = 0) → c * ∑ b : B, v b ^ 2 ≤ CoxeterGroup.bilinForm M v v

For an indecomposable positive semidefinite Coxeter form $B$ (i.e. an affine type), the form becomes positive definite (coercive) when restricted to vectors supported on any proper subset $I \subsetneq B$ of simple reflections. This is the "spherical-on-parabolics" reduction.

theorem AffineCoxeterHypProof.roots_integer_coords_of_crystallographic {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hCrys : IsCrystallographic M) (α : B → ℝ) : α ∈ TitsCone.standardΦpos M → ∀ (b : B), ∃ (n : ℤ), α b = ↑n

For a crystallographic Coxeter matrix, every positive root $\alpha \in \Phi^+$ has integer coordinates in the simple-root basis: $\alpha = \sum_b n_b \alpha_b$ with $n_b \in \mathbb Z$.

noncomputable def AffineCoxeterHypProof.AffineCoxeterHyp.mk' {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hAff : IsAffineCoxeter M) (hCrys : IsCrystallographic M) : TitsCone.AffineCoxeterHyp M

Constructor: an affine Coxeter matrix that is additionally crystallographic satisfies the hypotheses AffineCoxeterHyp (coercivity on proper parabolics + integral root coordinates) needed for the rest of the affine theory.