theorem linkComplex_maximal_union_maximal {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (C : Finset V) (hC : (b.linkComplex σ hσ).IsMaximal C) : b.IsMaximal (σ ∪ C)

If $C$ is maximal in the link complex $\mathrm{lk}_\sigma(\mathcal{B})$, then $\sigma \cup C$ is a chamber (maximal face) of the ambient building.

theorem coxeter_star_gallery_projection {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (hσA : σ ∈ A.faces) (C D : Finset V) (hC_link : C ∈ (b.linkComplex σ hσ).faces) (hD_link : D ∈ (b.linkComplex σ hσ).faces) (hC_max : (b.linkComplex σ hσ).IsMaximal C) (hD_max : (b.linkComplex σ hσ).IsMaximal D) (g : Gallery b.toSimplicialComplex) (hg_conn : g.Connects (σ ∪ C) (σ ∪ D)) (hg_in_A : ∀ E ∈ g.chambers, E ∈ A.faces) (hg_min : g.length = galleryDist b.toSimplicialComplex (σ ∪ C) (σ ∪ D)) : ∃ (g' : Gallery (b.linkComplex σ hσ)), g'.Connects C D ∧ g'.length ≤ g.length

Coxeter star projection: a minimal gallery in an apartment between chambers $\sigma \cup C$ and $\sigma \cup D$ projects to a gallery in the link $\mathrm{lk}_\sigma$ from $C$ to $D$ of no greater length.

theorem union_ne_of_disjoint_ne {V : Type} [DecidableEq V] (σ C D : Finset V) (hC_disj : Disjoint σ C) (hD_disj : Disjoint σ D) (hne : C ≠ D) : σ ∪ C ≠ σ ∪ D

If $C, D$ are each disjoint from $\sigma$ and $C \neq D$, then $\sigma \cup C \neq \sigma \cup D$.

theorem link_gallery_dist_le_axiom {V : Type} [DecidableEq V] (b : Building V) (σ : Finset V) (hσ : σ ∈ b.faces) (hσ_proper : ∃ (C : Finset V), b.IsMaximal C ∧ σ ⊂ C) (link_cc : ChamberComplex V) (h_link_cc : link_cc.toSimplicialComplex = b.linkComplex σ hσ) (C D : Finset V) (hC_max : (b.linkComplex σ hσ).IsMaximal C) (hD_max : (b.linkComplex σ hσ).IsMaximal D) : galleryDist link_cc.toSimplicialComplex C D ≤ galleryDist b.toSimplicialComplex (σ ∪ C) (σ ∪ D)

Axiom-form of the link distance bound: the gallery distance in the link $\mathrm{lk}_\sigma$ between maximal faces $C, D$ is bounded by the gallery distance between the chambers $\sigma \cup C, \sigma \cup D$ in the ambient building.