theorem coxeter_panel_generator {V : Type u_1} [DecidableEq V] (A : SimplicialComplex V) {B_idx : Type} (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hφ_inj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hφ_surj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hφ_adj : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (C : Finset V) (hC : A.IsMaximal C) (i : B_idx) : ∃ (D : Finset V), A.Adjacent C D ∧ φ D = φ C * M.toCoxeterSystem.simple i

Panel generator: in a Coxeter complex, every chamber $C$ has a chamber $D$ adjacent across the $i$-th panel with $\varphi(D) = \varphi(C) \cdot s_i$.

theorem coxeter_complex_backward_adj {V : Type u_1} [DecidableEq V] (A : SimplicialComplex V) {B_idx : Type} (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hφ_inj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hφ_surj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hφ_adj : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (C D : Finset V) (hC : A.IsMaximal C) (hD : A.IsMaximal D) (hne : C ≠ D) (h_cadj : CoxeterComplex.ChamberAdjacent M (φ C) (φ D)) : A.Adjacent C D

Backward direction: if $\varphi(C), \varphi(D)$ are chamber-adjacent in the Coxeter group and $C \neq D$, then $C, D$ are adjacent in the apartment.

theorem coxeter_adj_backward_in_apt {V : Type u_1} [DecidableEq V] (A : SimplicialComplex V) {B_idx : Type} (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hφ_inj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hφ_surj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hφ_adj : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (C D : Finset V) (hC : A.IsMaximal C) (hD : A.IsMaximal D) (h_cadj : CoxeterComplex.ChamberAdjacent M (φ C) (φ D)) : A.Adjacent C D

Coxeter chamber-adjacency lifts to apartment adjacency (the $C \neq D$ side condition is automatic from the Coxeter adjacency).

theorem retraction_has_vertex_map {V : Type u_1} [DecidableEq V] {b : Building V} (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (ρbar : Finset V → Finset V) (hρbar_max : ∀ (D : Finset V), A.IsMaximal (ρbar D)) : ∃ (σ : V → V), (∀ (C : Finset V), b.IsMaximal C → Finset.image σ C = ρbar C) ∧ ∀ (F C : Finset V), b.IsFacet F C → A.IsFacet (Finset.image σ F) (ρbar C)

The chamber-level retraction $\bar\rho$ is induced by a vertex map $\sigma : V \to V$ sending facets to facets.

theorem retraction_facet_shared_or_collapsed {V : Type u_1} [DecidableEq V] {b : Building V} (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (ρbar : Finset V → Finset V) (hρbar_max : ∀ (D : Finset V), A.IsMaximal (ρbar D)) (D₁ D₂ : Finset V) (h_adj : b.Adjacent D₁ D₂) (h_ne : ρbar D₁ ≠ ρbar D₂) : ∃ (F : Finset V), A.IsFacet F (ρbar D₁) ∧ A.IsFacet F (ρbar D₂)

For adjacent chambers $D_1, D_2$ with $\bar\rho(D_1) \neq \bar\rho(D_2)$, the images share a common facet in the apartment $A$.

theorem retraction_adj_or_eq_apt {V : Type u_1} [DecidableEq V] {b : Building V} (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (ρbar : Finset V → Finset V) (hρbar_max : ∀ (D : Finset V), A.IsMaximal (ρbar D)) (D₁ D₂ : Finset V) (h_adj : b.Adjacent D₁ D₂) : ρbar D₁ = ρbar D₂ ∨ A.Adjacent (ρbar D₁) (ρbar D₂)

Under the retraction $\bar\rho$, adjacent chambers either collapse to the same image or remain adjacent in the apartment.

theorem retraction_delta_adj_or_eq {V : Type u_1} [DecidableEq V] {b : Building V} (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (ρbar : Finset V → Finset V) (hρbar_max : ∀ (D : Finset V), A.IsMaximal (ρbar D)) {B_idx : Type} {M : CoxeterMatrix B_idx} (φ : Finset V → M.Group) (hφ_inj : ∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) (hφ_surj : ∀ (w : M.Group), ∃ (C : Finset V), A.IsMaximal C ∧ φ C = w) (hφ_adj : ∀ (C C' : Finset V), A.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (D₁ D₂ : Finset V) (h_adj : b.Adjacent D₁ D₂) : φ (ρbar D₁) = φ (ρbar D₂) ∨ CoxeterComplex.ChamberAdjacent M (φ (ρbar D₁)) (φ (ρbar D₂))

At the level of the Coxeter labeling $\varphi$, the images of adjacent chambers under $\bar\rho$ are either equal or chamber-adjacent.

theorem retraction_adj_preserves {V : Type u_1} [DecidableEq V] {b : Building V} (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (ρbar : Finset V → Finset V) (hρbar_max : ∀ (D : Finset V), A.IsMaximal (ρbar D)) (D₁ D₂ : Finset V) (h_adj : b.Adjacent D₁ D₂) : ρbar D₁ = ρbar D₂ ∨ A.Adjacent (ρbar D₁) (ρbar D₂)

The retraction $\bar\rho$ preserves adjacency: images of adjacent chambers are either equal or adjacent in $A$.

theorem canonical_retraction_delta_preserving {V : Type u_1} [DecidableEq V] {b : Building V} {W : Type u_2} [Group W] (delta : Finset V → Finset V → W) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) : ∃ (ρ : Finset V → Finset V), (∀ (D : Finset V), b.IsMaximal D → ρ D ∈ A.faces ∧ A.IsMaximal (ρ D)) ∧ ∀ (D : Finset V), b.IsMaximal D → delta C (ρ D) = delta C D

Existence of a canonical retraction $\rho$ that lands in $A$ and preserves the $\delta$-distance from $C$.

theorem label_uniqueness_retraction_agreement {V : Type u_1} [DecidableEq V] {b : Building V} {W : Type u_2} [Group W] (delta : Finset V → Finset V → W) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) (ρ : Finset V → Finset V) (hρ_max : ∀ (D : Finset V), b.IsMaximal D → ρ D ∈ A.faces ∧ A.IsMaximal (ρ D)) (hρ_delta : ∀ (D : Finset V), b.IsMaximal D → delta C (ρ D) = delta C D) (Y : Set (Finset V)) (f : Finset V → Finset V) (hY : ∀ y ∈ Y, b.IsMaximal y) (hf_img : ∀ y ∈ Y, f y ∈ A.faces) (hf_delta : ∀ y₁ ∈ Y, ∀ y₂ ∈ Y, delta (f y₁) (f y₂) = delta y₁ y₂) (y : Finset V) : y ∈ Y → ρ y = f y

Uniqueness of retractions: a $\delta$-preserving retraction $\rho$ must agree on $Y$ with any other $\delta$-preserving partial map $f$.

theorem retraction_label_agreement {V : Type u_1} [DecidableEq V] {b : Building V} {W : Type u_2} [Group W] (delta : Finset V → Finset V → W) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) (Y : Set (Finset V)) (f : Finset V → Finset V) (hY : ∀ y ∈ Y, b.IsMaximal y) (hf_img : ∀ y ∈ Y, f y ∈ A.faces) (hf_delta : ∀ y₁ ∈ Y, ∀ y₂ ∈ Y, delta (f y₁) (f y₂) = delta y₁ y₂) : ∃ (ρbar : Finset V → Finset V), (∀ (D : Finset V), b.IsMaximal D → ρbar D ∈ A.faces ∧ A.IsMaximal (ρbar D)) ∧ (∀ (D : Finset V), b.IsMaximal D → delta C (ρbar D) = delta C D) ∧ ∀ y ∈ Y, ρbar y = f y

Combined statement: there exists a canonical retraction $\bar\rho$ that agrees with any $\delta$-preserving partial map $f$ on its domain $Y$.

theorem delta_preserving_map_center_compat {V : Type u_1} [DecidableEq V] {b : Building V} {W : Type u_2} [Group W] (delta : Finset V → Finset V → W) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) (Y : Set (Finset V)) (f : Finset V → Finset V) (hY : ∀ y ∈ Y, b.IsMaximal y) (hf_img : ∀ y ∈ Y, f y ∈ A.faces) (hf_delta : ∀ y₁ ∈ Y, ∀ y₂ ∈ Y, delta (f y₁) (f y₂) = delta y₁ y₂) : (∀ y ∈ Y, delta C (f y) = delta C y) ∧ ∀ y ∈ Y, A.IsMaximal (f y)

Compatibility of a $\delta$-preserving map $f$ with the center chamber $C$: $f$ preserves $\delta(C, -)$ on $Y$, and its image is maximal in $A$.

theorem delta_injective_in_apt_generic {V : Type u_1} [DecidableEq V] {b : Building V} {W : Type u_2} [Group W] (delta : Finset V → Finset V → W) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C D₁ D₂ : Finset V) (hC : A.IsMaximal C) (hD₁_mem : D₁ ∈ A.faces) (hD₁ : A.IsMaximal D₁) (hD₂_mem : D₂ ∈ A.faces) (hD₂ : A.IsMaximal D₂) (h_delta_compat : ∃ (B_idx : Type) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group), (∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) ∧ ∃ (iso : W ≃* M.Group), ∀ (C D : Finset V), C ∈ A.faces → A.IsMaximal C → D ∈ A.faces → A.IsMaximal D → iso (delta C D) = (φ C)⁻¹ * φ D) (h_eq : delta C D₁ = delta C D₂) : D₁ = D₂

Injectivity of $\delta$ in an apartment: assuming a Coxeter compatibility, $\delta(C, D_1) = \delta(C, D_2)$ forces $D_1 = D_2$.

theorem retraction_agrees_with_delta_preserving {V : Type u_1} [DecidableEq V] {b : Building V} {W : Type u_2} [Group W] (delta : Finset V → Finset V → W) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C : Finset V) (hC : A.IsMaximal C) (ρbar : Finset V → Finset V) (hρ_max : ∀ (D : Finset V), b.IsMaximal D → ρbar D ∈ A.faces ∧ A.IsMaximal (ρbar D)) (hρ_fix : ∀ D ∈ A.faces, A.IsMaximal D → ρbar D = D) (hρ_delta : ∀ (D : Finset V), b.IsMaximal D → delta C (ρbar D) = delta C D) (Y : Set (Finset V)) (f : Finset V → Finset V) (hY : ∀ y ∈ Y, b.IsMaximal y) (hf_img : ∀ y ∈ Y, f y ∈ A.faces) (hf_delta : ∀ y₁ ∈ Y, ∀ y₂ ∈ Y, delta (f y₁) (f y₂) = delta y₁ y₂) (h_delta_compat : ∃ (B_idx : Type) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group), (∀ (C : Finset V), A.IsMaximal C → ∀ (D : Finset V), A.IsMaximal D → φ C = φ D → C = D) ∧ ∃ (iso : W ≃* M.Group), ∀ (C D : Finset V), C ∈ A.faces → A.IsMaximal C → D ∈ A.faces → A.IsMaximal D → iso (delta C D) = (φ C)⁻¹ * φ D) (y : Finset V) : y ∈ Y → ρbar y = f y

Any $\delta$-preserving retraction $\bar\rho$ which fixes the apartment agrees on $Y$ with any other $\delta$-preserving partial map $f$.