structure OppositeChamberHyp {V : Type u_1} [DecidableEq V] (b : Building V) : Prop

Hypothesis bundle for the opposite-chamber theorem: collects the ingredients about reversible foldings, distance equality between apartment and building, fold-decreasing distance, fold-preserved maximality, additive wall-separation distances, and the existence of galleries passing through a chosen chamber.

• apt_reversible_foldings (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (f : cc.Folding), ∃ (f' : cc.Folding), (∀ (D : Finset V), cc.IsMaximal D → (Finset.image f.morph.toFun D = D ↔ Finset.image f'.morph.toFun D ≠ D)) ∧ ∀ (D : Finset V), cc.IsMaximal D → Finset.image f.morph.toFun D = D → Finset.image f.morph.toFun (Finset.image f'.morph.toFun D) = D
• apt_dist_eq (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ (C D : Finset V), C ∈ A.faces → D ∈ A.faces → A.IsMaximal C → A.IsMaximal D → galleryDist A C D = galleryDist b.toSimplicialComplex C D
• fold_decreases_dist (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (f : cc.Folding) (C D : Finset V), cc.IsMaximal C → cc.IsMaximal D → Finset.image f.morph.toFun C = C → Finset.image f.morph.toFun D ≠ D → galleryDist cc.toSimplicialComplex C (Finset.image f.morph.toFun D) < galleryDist cc.toSimplicialComplex C D
• fold_preserves_maximal (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (f : cc.Folding) (D : Finset V), cc.IsMaximal D → cc.IsMaximal (Finset.image f.morph.toFun D)
• wall_sep_additive_dist (A : SimplicialComplex V) : A ∈ b.apartmentSystem.apartments → ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (C D C' : Finset V), cc.IsMaximal C → cc.IsMaximal D → cc.IsMaximal C' → (∀ (f : cc.Folding), ChamberComplex.OppositeSides f C D) → galleryDist cc.toSimplicialComplex C D = galleryDist cc.toSimplicialComplex C C' + galleryDist cc.toSimplicialComplex C' D
• gallery_through_chamber (C C' D : Finset V) : b.IsMaximal C → b.IsMaximal C' → b.IsMaximal D → galleryDist b.toSimplicialComplex C D = galleryDist b.toSimplicialComplex C C' + galleryDist b.toSimplicialComplex C' D → ∃ (g : Gallery b.toSimplicialComplex), g.Connects C D ∧ g.length = galleryDist b.toSimplicialComplex C D ∧ C' ∈ g.chambers

theorem wall_separates_opposite {V : Type u_1} [DecidableEq V] {b : Building V} (hyp : OppositeChamberHyp b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C D : Finset V) (hC : C ∈ A.faces) (hD : D ∈ A.faces) (hCmax : A.IsMaximal C) (hDmax : A.IsMaximal D) (hopp : AreOpposite b.toSimplicialComplex C D) (cc : ChamberComplex V) (hcc : cc.toSimplicialComplex = A) (f : cc.Folding) : ChamberComplex.OppositeSides f C D

For opposite chambers $C, D$ in a spherical apartment, every folding $f$ separates $C$ from $D$ (i.e. exactly one of them lies on the fixed side).

theorem chamber_in_minimal_gallery_of_opposite {V : Type u_1} [DecidableEq V] {b : Building V} (hyp : OppositeChamberHyp b) (A : SimplicialComplex V) (hA : A ∈ b.apartmentSystem.apartments) (C D : Finset V) (hC : C ∈ A.faces) (hD : D ∈ A.faces) (hCmax : A.IsMaximal C) (hDmax : A.IsMaximal D) (hopp : AreOpposite b.toSimplicialComplex C D) (cc : ChamberComplex V) (hcc : cc.toSimplicialComplex = A) (C' : Finset V) (hC' : C' ∈ A.faces) (hC'max : A.IsMaximal C') : ∃ (g : Gallery b.toSimplicialComplex), g.Connects C D ∧ g.length = galleryDist b.toSimplicialComplex C D ∧ C' ∈ g.chambers

Every chamber $C'$ of the apartment lies on some minimal gallery between opposite chambers $C, D$: the convex hull of an opposite pair is the entire apartment.