theorem List.chain_forall_of_head {α : Type u_2} {R : α → α → Prop} {P : α → Prop} (l : List α) (hne : l ≠ []) (hchain : IsChain R l) (hhead : P (l.head hne)) (hprop : ∀ (a b : α), R a b → P a → P b) (x : α) : x ∈ l → P x

Propagate a head-property along an IsChain: if $P$ holds at the head and is preserved by $R$-steps, then $P$ holds at every element of the list.

structure ChamberComplex.Folding {V : Type u_1} [DecidableEq V] (X : ChamberComplex V) : Type u_1

A folding of a chamber complex $X$: an idempotent simplicial endomorphism that maps chambers to chambers and facets to facets, is not the identity, is two-to-one on its fixed half-apartment, has a boundary edge (a fixed chamber adjacent to a moved one), and along any gallery between two fixed chambers any "moved" chamber forces an exit edge from the fixed half. Also requires stutter_at_boundary: a moved chamber adjacent to a fixed one is mapped to that fixed chamber. The final clause excludes stutters in minimal galleries between fixed chambers.

• morph : X.Morphism X.toSimplicialComplex
• chamberMap : self.morph.IsChamberMap
• preservesFacets : self.morph.PreservesFacets
• idempotent (v : V) : self.morph.toFun (self.morph.toFun v) = self.morph.toFun v
• not_id : ∃ (C : Finset V), X.IsMaximal C ∧ Finset.image self.morph.toFun C ≠ C
• twoToOne (C : Finset V) : X.IsMaximal C → Finset.image self.morph.toFun C = C → ∃! D : Finset V, X.IsMaximal D ∧ D ≠ C ∧ Finset.image self.morph.toFun D = C
• exists_boundary : ∃ (C : Finset V) (D : Finset V), X.Adjacent C D ∧ Finset.image self.morph.toFun C = C ∧ Finset.image self.morph.toFun D ≠ D
• gallery_exits (C D : Finset V) : X.IsMaximal C → Finset.image self.morph.toFun C = C → X.IsMaximal D → Finset.image self.morph.toFun D = D → ∀ (g : Gallery X.toSimplicialComplex), g.Connects C D → ∀ E ∈ g.chambers, Finset.image self.morph.toFun E ≠ E → ∃ (Ci : Finset V) (Ci1 : Finset V), Ci ∈ g.chambers ∧ Ci1 ∈ g.chambers ∧ X.Adjacent Ci Ci1 ∧ (X.IsMaximal Ci ∧ Finset.image self.morph.toFun Ci = Ci) ∧ ¬(X.IsMaximal Ci1 ∧ Finset.image self.morph.toFun Ci1 = Ci1)
• stutter_at_boundary (Ci Ci1 : Finset V) : X.Adjacent Ci Ci1 → X.IsMaximal Ci ∧ Finset.image self.morph.toFun Ci = Ci → Finset.image self.morph.toFun Ci1 ≠ Ci1 → Finset.image self.morph.toFun Ci1 = Ci
• stutter_contradicts_minimality (C D : Finset V) : X.IsMaximal C → Finset.image self.morph.toFun C = C → X.IsMaximal D → Finset.image self.morph.toFun D = D → ∀ (g : Gallery X.toSimplicialComplex), g.Connects C D → g.length = galleryDist X.toSimplicialComplex C D → ∀ (Ci Ci1 : Finset V), Ci ∈ g.chambers → Ci1 ∈ g.chambers → X.Adjacent Ci Ci1 → Finset.image self.morph.toFun Ci1 = Finset.image self.morph.toFun Ci → False

def ChamberComplex.Folding.fixedChambers {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (f : X.Folding) : Set (Finset V)

The set of chambers fixed (as sets) by the folding $f$, i.e. $f(C) = C$.

def ChamberComplex.Folding.movedChambers {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (f : X.Folding) : Set (Finset V)

The set of chambers moved by the folding $f$, i.e. $f(C) \neq C$.

theorem ChamberComplex.Folding.fixed_or_moved {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (f : X.Folding) {C : Finset V} (hC : X.IsMaximal C) : C ∈ f.fixedChambers ∨ C ∈ f.movedChambers

Every chamber is either fixed or moved by $f$.

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

The image $f(C)$ of any chamber is a fixed chamber (by idempotence).

theorem ChamberComplex.Folding.fixes_pointwise {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (f : X.Folding) {C : Finset V} (hfC : Finset.image f.morph.toFun C = C) (v : V) : v ∈ C → f.morph.toFun v = v

If $f(C) = C$ as a set, then $f$ fixes every vertex of $C$ pointwise.

theorem ChamberComplex.Folding.fold_adj_to_self {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (f : X.Folding) (hThin : X.IsThin) {C D : Finset V} (hadj : X.Adjacent C D) (hfC : Finset.image f.morph.toFun C = C) (hfD : Finset.image f.morph.toFun D ≠ D) : Finset.image f.morph.toFun D = C

In a thin chamber complex, a folding sends a moved chamber adjacent to a fixed chamber $C$ back onto $C$: $f(D) = C$.

structure ChamberComplex.ReversibleFolding {V : Type u_1} [DecidableEq V] (X : ChamberComplex V) : Type u_1

A reversible folding is a pair $(f, g)$ of foldings such that $f$'s fixed chambers equal $g$'s moved chambers (and vice versa), and the two foldings exchange the two boundary chambers of any wall: $g(C) = C'$ where $C, C'$ are an adjacent fixed/moved pair under $f$.

• f : X.Folding
• g : X.Folding
• complementary_fixed : self.f.fixedChambers = self.g.movedChambers
• complementary_moved : self.f.movedChambers = self.g.fixedChambers
• opposite_action (C C' : Finset V) : X.IsMaximal C → X.IsMaximal C' → C ≠ C' → Finset.image self.f.morph.toFun C = C → Finset.image self.f.morph.toFun C' = C → Finset.image self.g.morph.toFun C = C'
• opposite_action' (C C' : Finset V) : X.IsMaximal C → X.IsMaximal C' → C ≠ C' → Finset.image self.g.morph.toFun C = C → Finset.image self.g.morph.toFun C' = C → Finset.image self.f.morph.toFun C = C'

theorem ChamberComplex.ReversibleFolding.halves_disjoint {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (rf : X.ReversibleFolding) (C : Finset V) : ¬(C ∈ rf.f.fixedChambers ∧ C ∈ rf.g.fixedChambers)

The two half-apartments of a reversible folding are disjoint: no chamber is fixed by both $f$ and $g$.

def ChamberComplex.Wall {V : Type u_1} [DecidableEq V] (X : ChamberComplex V) (f : X.Folding) : Set (Finset V)

The wall of a folding $f$: faces fixed pointwise by $f$ that lie in some moved chamber.

def ChamberComplex.reflectionFun {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (rf : X.ReversibleFolding) : V → V

The vertex-level reflection associated with a reversible folding: at each vertex, apply $g$ where $f$ fixes, and $f$ elsewhere.

def ChamberComplex.OppositeSides {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (f : X.Folding) (C D : Finset V) : Prop

Two chambers lie on opposite sides of the wall of $f$: one is fixed and the other moved.

def ChamberComplex.SameSide {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (f : X.Folding) (C D : Finset V) : Prop

Two chambers lie on the same side of the wall of $f$: both fixed or both moved.

theorem ChamberComplex.reflection_involutive {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (rf : X.ReversibleFolding) (hfg : ∀ (v : V), rf.f.morph.toFun v = v → rf.f.morph.toFun (rf.g.morph.toFun v) = v) (hgf : ∀ (v : V), rf.g.morph.toFun v = v → rf.g.morph.toFun (rf.f.morph.toFun v) = v) (hcover : ∀ (v : V), rf.f.morph.toFun v = v ∨ rf.g.morph.toFun v = v) (v : V) : reflectionFun rf (reflectionFun rf v) = v

Under the cover / cross-fixed-point hypotheses, the reflection map associated with a reversible folding is an involution: $\rho \circ \rho = \mathrm{id}$.

structure ChamberComplex.WallReflection {V : Type u_1} [DecidableEq V] (X : ChamberComplex V) : Type u_1

A wall reflection: a reversible folding equipped with the cross-fixing and cover axioms needed to make its associated reflection a well-defined involution.

• rf : X.ReversibleFolding
• fg_id (v : V) : self.rf.f.morph.toFun v = v → self.rf.f.morph.toFun (self.rf.g.morph.toFun v) = v
• gf_id (v : V) : self.rf.g.morph.toFun v = v → self.rf.g.morph.toFun (self.rf.f.morph.toFun v) = v
• cover (v : V) : self.rf.f.morph.toFun v = v ∨ self.rf.g.morph.toFun v = v

def ChamberComplex.WallReflection.refl {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (s : X.WallReflection) : V → V

The reflection map of a wall reflection.

def ChamberComplex.WallReflection.wall {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (s : X.WallReflection) : Set (Finset V)

The wall (fixed set) of a wall reflection, viewed as a set of faces.

theorem ChamberComplex.WallReflection.refl_involutive {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (s : X.WallReflection) (v : V) : s.refl (s.refl v) = v

The wall reflection $\rho$ is an involution: $\rho \circ \rho = \mathrm{id}$.

theorem ChamberComplex.WallReflection.refl_injective {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (s : X.WallReflection) : Function.Injective s.refl

The wall reflection is injective.

theorem ChamberComplex.WallReflection.refl_surjective {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (s : X.WallReflection) : Function.Surjective s.refl

The wall reflection is surjective.

theorem ChamberComplex.WallReflection.refl_bijective {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (s : X.WallReflection) : Function.Bijective s.refl

The wall reflection is bijective.

theorem ChamberComplex.thin_implies_atMostTwo {V : Type u_1} [DecidableEq V] {X : ChamberComplex V} (hThin : X.IsThin) : X.AtMostTwoChambers

Thinness implies the "at most two chambers per facet" property used by the uniqueness lemma.