def ChamberComplex.FixesPointwise {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (f : K.Morphism K.toSimplicialComplex) (C : Finset V) : Prop

f fixes $C$ pointwise: $f(v) = v$ for every $v \in C$.

def ChamberComplex.ImageGalleryStutters {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (f : K.Morphism K.toSimplicialComplex) (cs : List (Finset V)) : Prop

The image of a gallery under $f$ stutters: some adjacent pair of chambers in the list has equal $f$-images.

theorem ChamberComplex.imageGalleryStutters_iff_galleryStuttersUnder {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (f : K.Morphism K.toSimplicialComplex) (cs : List (Finset V)) : ImageGalleryStutters f cs ↔ SimplicialComplex.GalleryStuttersUnder cs f.toFun

Equivalence between the two formulations of "the image gallery stutters".

theorem ChamberComplex.uniqueness_lemma_book {V : Type u_1} [DecidableEq V] {K : ChamberComplex V} (hThin : K.IsThin) (f : K.Morphism K.toSimplicialComplex) (hfCM : f.IsChamberMap) (C₀ : Finset V) (_hC₀ : K.IsMaximal C₀) (hfix₀ : FixesPointwise f C₀) (γ : Gallery K.toSimplicialComplex) (hstart : γ.chambers.head? = some C₀) : ImageGalleryStutters f γ.chambers ∨ ∀ C ∈ γ.chambers, FixesPointwise f C

Book's uniqueness lemma (3.3/3.5): in a thin chamber complex, if $f$ is a chamber map fixing the starting chamber $C_0$ pointwise, then along any gallery $\gamma$ starting at $C_0$, either $f \circ \gamma$ stutters or $f$ fixes every chamber of $\gamma$ pointwise.