theorem TitsTheoremProof.sufficient_foldings_fix_fold {V : Type u_1} [DecidableEq V] (cc : ChamberComplex V) (hsf : AptIsCoxeterProof.HasSufficientFoldings cc) (C C' : Finset V) (hadj : cc.Adjacent C C') : ∃ (f : cc.Folding), Finset.image f.morph.toFun C = C ∧ Finset.image f.morph.toFun C' = C

For adjacent chambers, the sufficient-foldings hypothesis yields a folding fixing $C$ and sending $C'$ to $C$.

theorem TitsTheoremProof.sufficient_foldings_fold_fix {V : Type u_1} [DecidableEq V] (cc : ChamberComplex V) (hsf : AptIsCoxeterProof.HasSufficientFoldings cc) (C C' : Finset V) (hadj : cc.Adjacent C C') : ∃ (f' : cc.Folding), Finset.image f'.morph.toFun C' = C' ∧ Finset.image f'.morph.toFun C = C'

Dual to sufficient_foldings_fix_fold: a folding fixing $C'$ and sending $C$ to $C'$.

theorem TitsTheoremProof.wallReflection_involutive {V : Type u_1} [DecidableEq V] (cc : ChamberComplex V) (s : cc.WallReflection) (v : V) : s.refl (s.refl v) = v

A wall reflection is involutive: $s(s(v)) = v$ for every vertex $v$.

theorem TitsTheoremProof.simple_ne_one {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (i : B) : M.toCoxeterSystem.simple i ≠ 1

A simple generator $s_i$ of a Coxeter group is not the identity.

theorem TitsTheoremProof.simple_inv {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (i : B) : (M.toCoxeterSystem.simple i)⁻¹ = M.toCoxeterSystem.simple i

Each simple generator is its own inverse: $s_i^{-1} = s_i$.

theorem TitsTheoremProof.mul_simple_ne_self {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (w : M.Group) (i : B) : w * M.toCoxeterSystem.simple i ≠ w

Right multiplication by a simple generator moves any element: $w s_i \ne w$.

theorem TitsTheoremProof.chamberAdjacent_left_mul {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (g w w' : M.Group) (hadj : CoxeterComplex.ChamberAdjacent M w w') : CoxeterComplex.ChamberAdjacent M (g * w) (g * w')

Chamber-adjacency in a Coxeter complex is invariant under left multiplication by any group element.

theorem TitsTheoremProof.chamberAdjacent_mul_simple {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (w : M.Group) (i : B) : CoxeterComplex.ChamberAdjacent M w (w * M.toCoxeterSystem.simple i)

The chambers $w$ and $w s_i$ are chamber-adjacent in the Coxeter complex.

def TitsTheoremProof.galleryPath {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (w : M.Group) : List B → List M.Group

The gallery path realizing the word $s_{i_1} \dots s_{i_n}$ starting from $w$: the list $[w, w s_{i_1}, w s_{i_1} s_{i_2}, \dots]$.

theorem TitsTheoremProof.galleryPath_nonempty {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (w : M.Group) (word : List B) : galleryPath M w word ≠ []

The gallery path is non-empty.

theorem TitsTheoremProof.word_gallery_isGallery {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (w : M.Group) : CoxeterComplex.IsGallery M (galleryPath M w word)

Every gallery path is a valid gallery in the Coxeter complex (consecutive chambers are chamber-adjacent).

def TitsTheoremProof.wordProduct {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (w : M.Group) : List B → M.Group

Accumulated word product: starting from $w$, multiply right by each simple generator $s_i$ in the word.

theorem TitsTheoremProof.galleryPath_last {B : Type u_2} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (word : List B) (w : M.Group) : (galleryPath M w word).getLast ⋯ = wordProduct M w word

The last chamber of the gallery path equals the word product.