structure CombinatorialGeometry.RetractionHalfApartmentConfig {V : Type u_1} [DecidableEq V] (b : Building V) : Type u_1

Configuration of data needed for the half-apartment retraction analysis: two adjacent chambers $C, C'$, a third chamber $D$, an apartment $A$ containing $C, C'$, two retractions $\rho, \rho'$ onto $A$ centered at $C, C'$, the two half-apartments $H, H'$ on either side of the wall, plus the wall reflection $s$.

• C : Finset V
• C' : Finset V
• D : Finset V
• hC : b.IsMaximal self.C
• hC' : b.IsMaximal self.C'
• hD : b.IsMaximal self.D
• hCC' : self.C ≠ self.C'
• hCD : self.C ≠ self.D
• hC'D : self.C' ≠ self.D
• adj : b.Adjacent self.C self.C'
• A : SimplicialComplex V
• hA : self.A ∈ b.apartmentSystem.apartments
• hCA : self.C ∈ self.A.faces
• hC'A : self.C' ∈ self.A.faces
• ρ : Finset V → Finset V
• ρ' : Finset V → Finset V
• ρ_maps_to_A (E : Finset V) : b.IsMaximal E → self.ρ E ∈ self.A.faces
• ρ'_maps_to_A (E : Finset V) : b.IsMaximal E → self.ρ' E ∈ self.A.faces
• ρ_preserves_dist_C (E : Finset V) : b.IsMaximal E → galleryDist b.toSimplicialComplex self.C (self.ρ E) = galleryDist b.toSimplicialComplex self.C E
• ρ'_preserves_dist_C' (E : Finset V) : b.IsMaximal E → galleryDist b.toSimplicialComplex self.C' (self.ρ' E) = galleryDist b.toSimplicialComplex self.C' E
• ρ_diminishes_dist_C' (E : Finset V) : b.IsMaximal E → galleryDist b.toSimplicialComplex self.C' (self.ρ E) ≤ galleryDist b.toSimplicialComplex self.C' E
• ρ'_diminishes_dist_C (E : Finset V) : b.IsMaximal E → galleryDist b.toSimplicialComplex self.C (self.ρ' E) ≤ galleryDist b.toSimplicialComplex self.C E
• H : Set (Finset V)
• H' : Set (Finset V)
• hC_in_H : self.C ∈ self.H
• hC'_in_H' : self.C' ∈ self.H'
• H_char (E : Finset V) : E ∈ self.A.faces → self.A.IsMaximal E → (E ∈ self.H ↔ galleryDist b.toSimplicialComplex self.C E < galleryDist b.toSimplicialComplex self.C' E)
• H'_char (E : Finset V) : E ∈ self.A.faces → self.A.IsMaximal E → (E ∈ self.H' ↔ galleryDist b.toSimplicialComplex self.C' E < galleryDist b.toSimplicialComplex self.C E)
• ρ_maximal (E : Finset V) : b.IsMaximal E → self.A.IsMaximal (self.ρ E)
• ρ'_maximal (E : Finset V) : b.IsMaximal E → self.A.IsMaximal (self.ρ' E)
• retraction_agree_on_common_apt : (∃ B ∈ b.apartmentSystem.apartments, self.C ∈ B.faces ∧ self.C' ∈ B.faces ∧ self.D ∈ B.faces) → self.ρ self.D = self.ρ' self.D
• adj_A : self.A.Adjacent self.C self.C'
• adj_dist : galleryDist b.toSimplicialComplex self.C self.C' = 1
• adj_dist' : galleryDist b.toSimplicialComplex self.C' self.C = 1
• adj_triangle : galleryDist b.toSimplicialComplex self.C' self.D ≤ galleryDist b.toSimplicialComplex self.C self.D + 1
• adj_triangle' : galleryDist b.toSimplicialComplex self.C self.D ≤ galleryDist b.toSimplicialComplex self.C' self.D + 1
• coxeter_dist_ne (E : Finset V) : E ∈ self.A.faces → self.A.IsMaximal E → galleryDist b.toSimplicialComplex self.C' E ≠ galleryDist b.toSimplicialComplex self.C E
• s_reflection : Finset V → Finset V
• s_swap_C : self.s_reflection self.C = self.C'
• s_swap_C' : self.s_reflection self.C' = self.C
• s_invol (E : Finset V) : self.s_reflection (self.s_reflection E) = E
• s_swaps_H (E : Finset V) : E ∈ self.H → self.s_reflection E ∈ self.H'
• s_reflection_eq_of_equal_dist : galleryDist b.toSimplicialComplex self.C' self.D = galleryDist b.toSimplicialComplex self.C self.D → self.s_reflection (self.ρ self.D) = self.ρ' self.D

theorem CombinatorialGeometry.retraction_case_further {V : Type u_1} [DecidableEq V] (b : Building V) (cfg : RetractionHalfApartmentConfig b) (hfurther : galleryDist b.toSimplicialComplex cfg.C' cfg.D > galleryDist b.toSimplicialComplex cfg.C cfg.D) : cfg.ρ cfg.D = cfg.ρ' cfg.D ∧ cfg.ρ cfg.D ∈ cfg.H

Case "further": if $d(C', D) > d(C, D)$, then $\rho D = \rho' D$ and this common image lies in the near half-apartment $H$.

theorem CombinatorialGeometry.retraction_case_closer {V : Type u_1} [DecidableEq V] (b : Building V) (cfg : RetractionHalfApartmentConfig b) (hcloser : galleryDist b.toSimplicialComplex cfg.C' cfg.D < galleryDist b.toSimplicialComplex cfg.C cfg.D) : cfg.ρ cfg.D = cfg.ρ' cfg.D ∧ cfg.ρ cfg.D ∈ cfg.H'

Case "closer": if $d(C', D) < d(C, D)$, then $\rho D = \rho' D$ and this common image lies in the far half-apartment $H'$.

theorem CombinatorialGeometry.retraction_case_equal {V : Type u_1} [DecidableEq V] (b : Building V) (cfg : RetractionHalfApartmentConfig b) (hequal : galleryDist b.toSimplicialComplex cfg.C' cfg.D = galleryDist b.toSimplicialComplex cfg.C cfg.D) : cfg.ρ cfg.D ∈ cfg.H' ∧ cfg.ρ' cfg.D ∈ cfg.H ∧ cfg.s_reflection (cfg.ρ cfg.D) = cfg.ρ' cfg.D

Case "equal": if $d(C', D) = d(C, D)$, then $\rho D \in H'$, $\rho' D \in H$, and the wall reflection $s$ swaps them: $s(\rho D) = \rho' D$.