def Gallery.IsNonStuttering {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} (g : Gallery K) : Prop

A gallery is non-stuttering if consecutive chambers are always distinct.

def GalleryType {V : Type u_1} [DecidableEq V] {L : Type u_2} [DecidableEq L] (K : ChamberComplex V) (lab : Labelling K.toSimplicialComplex L) (g : Gallery K.toSimplicialComplex) : List (Finset L)

The type of a gallery under a labelling: the list of label-sets of the shared codim-$1$ faces along consecutive chambers.

structure ChamberComplex.IsCoxeterCharacterized {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) : Prop

$K$ is Coxeter-characterized: it is thin and every adjacent pair has a folding that separates them (one fixed, one moved).

• thin : K.IsThin
• wallSeparation (C D : Finset V) : K.Adjacent C D → ∃ (f : K.Folding), Finset.image f.morph.toFun C = C ∧ Finset.image f.morph.toFun D ≠ D ∨ Finset.image f.morph.toFun D = D ∧ Finset.image f.morph.toFun C ≠ C

def ChamberComplex.HasTypeDeletion {V : Type u_1} [DecidableEq V] {L : Type u_2} [DecidableEq L] (K : ChamberComplex V) (lab : Labelling K.toSimplicialComplex L) : Prop

The type-deletion condition for galleries: any non-minimal non-stuttering gallery admits a shorter gallery whose type is obtained by deleting two letters at positions $i < j$ from the original type, mirroring the Coxeter deletion condition.