structure SimplicialComplex (V : Type u_2) [DecidableEq V] : Type u_2

An abstract simplicial complex on a vertex set $V$: a downward-closed family of nonempty finite subsets ("faces") of $V$.

• faces : Set (Finset V)
• nonempty_of_mem (s : Finset V) : s ∈ self.faces → s.Nonempty
• down_closed {s t : Finset V} : s ∈ self.faces → t ⊆ s → t.Nonempty → t ∈ self.faces

def SimplicialComplex.IsFace {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (y x : Finset V) : Prop

y is a face of x in K: both are faces of $K$ and $y ⊆ x$.

def SimplicialComplex.IsFacet {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (y x : Finset V) : Prop

y is a codimension-$1$ face ("facet") of x in K: $y$ is a face of $x$ with $|x \setminus y| = 1$.

def SimplicialComplex.IsMaximal {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (x : Finset V) : Prop

x is a maximal face ("chamber") of K: a face contained in no strictly larger face.

def SimplicialComplex.Adjacent {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (C D : Finset V) : Prop

Two distinct chambers $C, D$ are adjacent if they share a common codim-$1$ facet $F$.

structure Gallery {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) : Type u_1

A gallery in K: a nonempty list of chambers in which consecutive entries are adjacent.

• chambers : List (Finset V)
• length_pos : self.chambers.length > 0
• all_maximal (C : Finset V) : C ∈ self.chambers → K.IsMaximal C
• adjacent_consecutive : List.IsChain K.Adjacent self.chambers

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

The combinatorial length of a gallery: number of edges = (number of chambers) $- 1$.

def Gallery.Connects {V : Type u_1} [DecidableEq V] {K : SimplicialComplex V} (g : Gallery K) (C D : Finset V) : Prop

The gallery g "connects" $C$ to $D$ if its first chamber is $C$ and its last chamber is $D$.

structure ChamberComplex (V : Type u_2) [DecidableEq V] extends SimplicialComplex V : Type u_2

A chamber complex: every face is contained in some chamber, and any two chambers are connected by a gallery.

• faces : Set (Finset V)
• nonempty_of_mem (s : Finset V) : s ∈ self.faces → s.Nonempty
• down_closed {s t : Finset V} : s ∈ self.faces → t ⊆ s → t.Nonempty → t ∈ self.faces
• exists_maximal (s : Finset V) : s ∈ self.faces → ∃ (C : Finset V), self.IsMaximal C ∧ s ⊆ C
• gallery_connected (C D : Finset V) : self.IsMaximal C → self.IsMaximal D → ∃ (g : Gallery self.toSimplicialComplex), g.chambers.head? = some C ∧ g.chambers.getLast? = some D

def ChamberComplex.IsThin {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) : Prop

K is thin if every codim-$1$ face $F$ of a chamber $C$ lies in exactly one other chamber.

def ChamberComplex.IsThick {V : Type u_1} [DecidableEq V] (K : ChamberComplex V) : Prop

K is thick if every codim-$1$ face $F$ of a chamber $C$ lies in at least two chambers distinct from $C$.

noncomputable def galleryDist {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (C D : Finset V) : ℕ

The combinatorial gallery distance $d(C,D)$ between chambers: $0$ if $C = D$, else the infimum length over all galleries connecting $C$ and $D$.

theorem galleryDist_self {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (C : Finset V) : galleryDist K C C = 0

Self-distance is zero: $d(C,C) = 0$.

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

Adjacency is symmetric: $C \sim D \implies D \sim C$.

theorem galleryDist_comm {V : Type u_1} [DecidableEq V] (K : SimplicialComplex V) (C D : Finset V) : galleryDist K C D = galleryDist K D C

Gallery distance is symmetric: $d(C,D) = d(D,C)$.