theorem ChamberComplex.adjacent_symm' {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} {C D : Finset V} (h : K.Adjacent C D) : K.Adjacent D C

Symmetry of chamber adjacency (local alias).

theorem ChamberComplex.image_is_fixed' {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (f : K.Folding) (C : Finset V) (hC : K.IsMaximal C) : Finset.image f.morph.toFun (Finset.image f.morph.toFun C) = Finset.image f.morph.toFun C

Idempotence at the chamber level: $f(f(C)) = f(C)$ for any chamber $C$.

theorem ChamberComplex.folding_maps_adj' {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (f : K.Folding) (C D : Finset V) (hadj : K.Adjacent C D) : Finset.image f.morph.toFun C = Finset.image f.morph.toFun D ∨ K.Adjacent (Finset.image f.morph.toFun C) (Finset.image f.morph.toFun D)

A folding maps an adjacent pair either to the same chamber (stutter) or to an adjacent pair.

theorem ChamberComplex.galleryDist_le_length' {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} (C D : Finset V) (g : Gallery K) (hconn : g.Connects C D) : galleryDist K C D ≤ g.length

Any connecting gallery bounds the gallery distance from above: $d(C,D) \leq \ell(g)$.

theorem ChamberComplex.galleryDist_eq_zero_imp {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (C D : Finset V) (hCmax : K.IsMaximal C) (hDmax : K.IsMaximal D) (h : galleryDist K.toSimplicialComplex C D = 0) : C = D

If two chambers have gallery distance $0$, they must be equal.

theorem ChamberComplex.exists_gallery_adj {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} {C D : Finset V} (hadj : K.Adjacent C D) : ∃ (g : Gallery K), g.Connects C D ∧ g.length = 1

Adjacent chambers admit a gallery of length $1$ connecting them.

theorem ChamberComplex.gallery_drop_first {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} (g : Gallery K) (C D : Finset V) (hconn : g.Connects C D) (hlen : g.length ≥ 1) : ∃ (C₁ : Finset V) (g' : Gallery K), g'.Connects C₁ D ∧ g'.length = g.length - 1 ∧ K.Adjacent C C₁ ∧ C₁ ∈ g.chambers ∧ ∀ X ∈ g'.chambers, X ∈ g.chambers

Drop the first chamber of a positive-length gallery to obtain a shorter gallery starting at the second chamber.

theorem ChamberComplex.folding_shortens_dist {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (f : K.Folding) (D E : Finset V) (hDmax : K.IsMaximal D) (hEmax : K.IsMaximal E) (hfD : Finset.image f.morph.toFun D = D) (hfE : Finset.image f.morph.toFun E ≠ E) : galleryDist K.toSimplicialComplex (Finset.image f.morph.toFun E) D < galleryDist K.toSimplicialComplex E D

Key folding inequality: if $f$ fixes $D$ but moves $E$, then $d(f(E), D) < d(E, D)$ — i.e. folding strictly decreases gallery distance to a fixed chamber.

theorem ChamberComplex.HalfApartmentDistChar {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (rf : K.ReversibleFolding) (C C' : Finset V) (hadj : K.Adjacent C C') (hC_fixed : C ∈ rf.f.fixedChambers) (hC'_moved : C' ∈ rf.f.movedChambers) : rf.f.fixedChambers = {D : Finset V | K.IsMaximal D ∧ galleryDist K.toSimplicialComplex C D < galleryDist K.toSimplicialComplex C' D}

Characterization of the half-apartment via gallery distance: for a reversible folding $f$ with adjacent boundary pair $C$ (fixed) and $C'$ (moved), the fixed half is exactly $\{D \text{ chamber} \mid d(C,D) < d(C',D)\}$.