theorem CombinatorialGeometry.retraction_dichotomy {V : Type u_1} [DecidableEq V] (b : Building V) (cfg : RetractionHalfApartmentConfig b) : cfg.ρ cfg.D = cfg.ρ' cfg.D ∨ cfg.ρ cfg.D = cfg.s_reflection (cfg.ρ' cfg.D) ∧ cfg.ρ cfg.D ∈ cfg.H' ∧ cfg.ρ' cfg.D ∈ cfg.H

Retraction dichotomy: for two retractions $\rho, \rho'$ associated to adjacent chambers $C, C'$ and a target chamber $D$, either $\rho D = \rho' D$ or $\rho D$ and $\rho' D$ are related by the wall reflection $s$ across $\{C, C'\}$ and lie in opposite half-apartments.