theorem ChamberComplex.coxeterReversibleFolding_exists {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), K.IsMaximal C → ∀ (D : Finset V), K.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), K.IsMaximal C ∧ φ C = w) (hadj_fwd : ∀ (C C' : Finset V), K.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (hadj_bwd : ∀ (C C' : Finset V), K.IsMaximal C → K.IsMaximal C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C') → K.Adjacent C C') (C D : Finset V) (hadj : K.Adjacent C D) : ∃ (rf : K.ReversibleFolding), C ∈ rf.f.fixedChambers ∧ D ∈ rf.g.fixedChambers

Existence of a reversible folding across any adjacent wall in a Coxeter-labelled complex: given a label $\varphi$ converting chamber adjacency to multiplication by a simple reflection in $W$, for each adjacent pair $(C, D)$ there is a reversible folding $(f, g)$ with $C$ in $f$'s fixed half and $D$ in $g$'s fixed half.

theorem ChamberComplex.coxeterReversibleFolding {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), K.IsMaximal C → ∀ (D : Finset V), K.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), K.IsMaximal C ∧ φ C = w) (hadj_fwd : ∀ (C C' : Finset V), K.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (hadj_bwd : ∀ (C C' : Finset V), K.IsMaximal C → K.IsMaximal C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C') → K.Adjacent C C') (C D : Finset V) (hadj : K.Adjacent C D) : ∃ (rf : K.ReversibleFolding), Finset.image rf.f.morph.toFun C = C ∧ Finset.image rf.f.morph.toFun D = C ∧ Finset.image rf.g.morph.toFun D = D ∧ Finset.image rf.g.morph.toFun C = D

Strong form of the Coxeter reversible folding: for any adjacent pair $(C, D)$, there is a reversible folding $(f, g)$ with $f(C) = C$, $f(D) = C$, $g(D) = D$, $g(C) = D$.

theorem ChamberComplex.coxeterComplex_facet_generator {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) (B_idx : Type) (M : CoxeterMatrix B_idx) (φ : Finset V → M.Group) (hinj : ∀ (C : Finset V), K.IsMaximal C → ∀ (D : Finset V), K.IsMaximal D → φ C = φ D → C = D) (hsurj : ∀ (w : M.Group), ∃ (C : Finset V), K.IsMaximal C ∧ φ C = w) (hadj_fwd : ∀ (C C' : Finset V), K.Adjacent C C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C')) (hadj_bwd : ∀ (C C' : Finset V), K.IsMaximal C → K.IsMaximal C' → CoxeterComplex.ChamberAdjacent M (φ C) (φ C') → K.Adjacent C C') (hfacet_shared : ∀ (F C : Finset V), K.IsFacet F C → K.IsMaximal C → ∃ (D : Finset V), D ≠ C ∧ K.IsMaximal D ∧ K.IsFacet F D) (F C : Finset V) (hFC : K.IsFacet F C) (hC : K.IsMaximal C) : ∃ (i : B_idx), ∀ (D : Finset V), K.IsMaximal D → φ D = φ C * M.toCoxeterSystem.simple i → K.IsFacet F D

For a facet $F \subset C$, the simple generator $s_i$ characterizing the other chamber across $F$ is uniquely determined and any chamber $D$ with $\varphi(D) = \varphi(C) s_i$ also has $F$ as a facet.