def WallReflectionAction.applyFunWord {V : Type u_1} [DecidableEq V] (word : List (V → V)) (C : Finset V) : Finset V

Apply a word of vertex maps (e.g. wall reflections) sequentially to a chamber $C$, taking images at each step.

theorem WallReflectionAction.adj_folding_fix_fold {V : Type u_1} [DecidableEq V] {cc : ChamberComplex V} (hsf : AptIsCoxeterProof.HasSufficientFoldings cc) {C D : Finset V} (hadj : cc.Adjacent C D) : ∃ (f : cc.Folding), Finset.image f.morph.toFun C = C ∧ Finset.image f.morph.toFun D = C

For adjacent chambers $C, D$, there is a folding fixing $C$ and sending $D$ to $C$.

theorem WallReflectionAction.gallery_step_has_folding {V : Type u_1} [DecidableEq V] {cc : ChamberComplex V} (hsf : AptIsCoxeterProof.HasSufficientFoldings cc) {C D : Finset V} (hadj : cc.Adjacent C D) : ∃ (f : cc.Folding), Finset.image f.morph.toFun C = C ∧ Finset.image f.morph.toFun D = C

Each step of a gallery (adjacent pair) admits a folding collapsing it.

theorem WallReflectionAction.gallery_chain_head_adj {V : Type u_1} [DecidableEq V] {cc : ChamberComplex V} {a b : Finset V} {rest : List (Finset V)} (hchain : List.IsChain cc.Adjacent (a :: b :: rest)) : cc.Adjacent a b

Extract the head adjacency from a gallery chain a :: b :: rest.

theorem WallReflectionAction.gallery_chain_tail {V : Type u_1} [DecidableEq V] {cc : ChamberComplex V} {a b : Finset V} {rest : List (Finset V)} (hchain : List.IsChain cc.Adjacent (a :: b :: rest)) : List.IsChain cc.Adjacent (b :: rest)

The tail of a gallery chain remains a gallery chain.

theorem WallReflectionAction.isChain_getElem_adj {α : Type u_2} {R : α → α → Prop} {l : List α} (hchain : List.IsChain R l) {i : ℕ} (hi : i + 1 < l.length) : R l[i] l[i + 1]

In a chain, consecutive elements are $R$-related at every index.

theorem WallReflectionAction.chain_foldings_exist {V : Type u_1} [DecidableEq V] {cc : ChamberComplex V} (hsf : AptIsCoxeterProof.HasSufficientFoldings cc) (cs : List (Finset V)) (hchain : List.IsChain cc.Adjacent cs) (hall : ∀ C ∈ cs, cc.IsMaximal C) : ∃ (fs : List cc.Folding), fs.length + 1 = cs.length ∨ cs.length = 0 ∧ fs = []

For any gallery of chambers, there exists a list of foldings (one per adjacency step) collapsing each step.