theorem chain_transition {α : Type u_1} (R : α → α → Prop) (P : α → Prop) (l : List α) (hchain : List.IsChain R l) (hl : l ≠ []) (hhead : P (l.head hl)) (hE : ∃ e ∈ l, ¬P e) : ∃ (a : α) (b : α), a ∈ l ∧ b ∈ l ∧ R a b ∧ P a ∧ ¬P b

Boundary-crossing principle: in a chain whose head satisfies $P$ but some entry does not, there exists an $R$-related adjacent pair witnessing the transition from $P$ to $\neg P$.

theorem ThicknessFoldings.apt_is_thin_pre {V : Type} [DecidableEq V] (K : ChamberComplex V) (pre : AptIsCoxeterProof.PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) (F C : Finset V) : A.IsFacet F C → A.IsMaximal C → ∃! D : Finset V, D ≠ C ∧ A.IsFacet F D ∧ A.IsMaximal D

Every apartment is thin: each facet $F \subset C$ lies in exactly one other chamber $D$ of the apartment.

theorem ThicknessFoldings.apt_automorphism_sending_chamber_pre {V : Type} [DecidableEq V] {K : ChamberComplex V} (pre : AptIsCoxeterProof.PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) (C : Finset V) (hC : A.IsMaximal C) (D : Finset V) (hD : A.IsMaximal D) : ∃ (φ : V → V), Function.Bijective φ ∧ (∀ (s : Finset V), s ∈ A.faces ↔ Finset.image φ s ∈ A.faces) ∧ Finset.image φ D = C

Chamber transitivity for the pre-apartment system: for any two chambers $C, D$ of an apartment, there is a bijective vertex map sending $C$ to $D$.

theorem ThicknessFoldings.bij_iso_fixing_chamber_is_id_pre {V : Type} [DecidableEq V] {K : ChamberComplex V} (pre : AptIsCoxeterProof.PreApartmentData K) (B B' : SimplicialComplex V) (hB : B ∈ pre.apartments) (D : Finset V) (hD_B : D ∈ B.faces) (hD_max : K.IsMaximal D) (φ : V → V) (hφ_bij : Function.Bijective φ) (_hφ_faces : ∀ (s : Finset V), s ∈ B.faces ↔ Finset.image φ s ∈ B'.faces) (hφ_D : Finset.image φ D = D) (s : Finset V) : s ∈ B.faces → Finset.image φ s = s

A bijective vertex map fixing a chamber pointwise is the identity on the apartment (pre-apartment version).

theorem ThicknessFoldings.iso_bijective_fixing_chamber_pre {V : Type} [DecidableEq V] {K : ChamberComplex V} (pre : AptIsCoxeterProof.PreApartmentData K) (B : SimplicialComplex V) (hB : B ∈ pre.apartments) (B₀ : SimplicialComplex V) (hB₀ : B₀ ∈ pre.apartments) (D : Finset V) (hD_B : D ∈ B.faces) (hD_B₀ : D ∈ B₀.faces) (hD_max_B : B.IsMaximal D) : ∃ (φ : V → V), Function.Bijective φ ∧ (∀ (s : Finset V), s ∈ B.faces ↔ Finset.image φ s ∈ B₀.faces) ∧ Finset.image φ D = D

Any apartment iso fixing a chamber is bijective (pre-apartment version).

theorem ThicknessFoldings.exists_canonical_retraction_pre {V : Type} [DecidableEq V] (K : ChamberComplex V) (pre : AptIsCoxeterProof.PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) (C : Finset V) (hC : A.IsMaximal C) : ∃ (ρ : V → V), (∀ s ∈ K.faces, Finset.image ρ s ∈ A.faces) ∧ (∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → ρ v = v) ∧ (∀ (D : Finset V), K.IsMaximal D → A.IsMaximal (Finset.image ρ D)) ∧ (∀ (D₁ D₂ : Finset V), K.Adjacent D₁ D₂ → Finset.image ρ D₁ = Finset.image ρ D₂ ∨ A.Adjacent (Finset.image ρ D₁) (Finset.image ρ D₂)) ∧ (∀ B ∈ pre.apartments, C ∈ B.faces → ∀ (v₁ v₂ : V), (∃ s ∈ B.faces, v₁ ∈ s) → (∃ s ∈ B.faces, v₂ ∈ s) → ρ v₁ = ρ v₂ → v₁ = v₂) ∧ (∀ (v : V), ∃ s ∈ A.faces, ρ v ∈ s) ∧ ∀ B ∈ pre.apartments, C ∈ B.faces → ∀ (σ : V → V), (∀ s ∈ K.faces, Finset.image σ s ∈ B.faces) → (∀ (v : V), (∃ s ∈ B.faces, v ∈ s) → σ v = v) → ∀ (v : V), (∃ s ∈ A.faces, v ∈ s) → ρ (σ v) = v

Existence of the canonical retraction $\rho_{D;C,A}$ for a pre-apartment system.

theorem ThicknessFoldings.apt_facet_of_maximal_containing_pre {V : Type} [DecidableEq V] (K : ChamberComplex V) (pre : AptIsCoxeterProof.PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) {C D F₀ : Finset V} (hC_max : A.IsMaximal C) (hD_max : A.IsMaximal D) (hF₀_C : A.IsFacet F₀ C) (hF₀_sub_D : F₀ ⊆ D) : A.IsFacet F₀ D

A facet $F$ contained in a maximal chamber $C$ of an apartment is a facet of $C$ in the apartment.

theorem ThicknessFoldings.thin_unique_other_chamber_pre {V : Type} [DecidableEq V] (K : ChamberComplex V) (pre : AptIsCoxeterProof.PreApartmentData K) {A : SimplicialComplex V} (hA : A ∈ pre.apartments) {F C D₁ D₂ : Finset V} (hC_max : A.IsMaximal C) (hF_C : A.IsFacet F C) (hD₁_max : A.IsMaximal D₁) (hD₁_ne : D₁ ≠ C) (hF_D₁ : A.IsFacet F D₁) (hD₂_max : A.IsMaximal D₂) (hD₂_ne : D₂ ≠ C) (hF_D₂ : A.IsFacet F D₂) : D₁ = D₂

Pre-apartment thinness: each facet $F$ has a unique other chamber $D$ besides $C$ in the apartment.

theorem ThicknessFoldings.apt_chamber_with_facet_is_C_or_C_pre {V : Type} [DecidableEq V] (K : ChamberComplex V) (pre : AptIsCoxeterProof.PreApartmentData K) {A : SimplicialComplex V} (hA : A ∈ pre.apartments) {C C' D F₀ : Finset V} (hC_max : A.IsMaximal C) (hC'_max : A.IsMaximal C') (hD_max : A.IsMaximal D) (hne : C ≠ C') (hF₀_C : A.IsFacet F₀ C) (hF₀_C' : A.IsFacet F₀ C') (hF₀_sub_D : F₀ ⊆ D) : D = C ∨ D = C'

A chamber of the apartment containing a facet $F$ is either $C$ or its unique opposite chamber across $F$.

theorem ThicknessFoldings.exists_map_fixing_sending_adj_pre {V : Type} [DecidableEq V] (K : ChamberComplex V) (hK_thick : K.IsThick) (pre : AptIsCoxeterProof.PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) (C C' : Finset V) (hC_A : A.IsMaximal C) (hC'_A : A.IsMaximal C') (hadj_A : A.Adjacent C C') : ∃ (f : V → V), Finset.image f C = C ∧ Finset.image f C' = C ∧ (∀ s ∈ A.faces, Finset.image f s ∈ A.faces) ∧ (∀ (v : V), f (f v) = f v) ∧ (∀ (D : Finset V), A.IsMaximal D → A.IsMaximal (Finset.image f D)) ∧ (∀ (F D : Finset V), A.IsFacet F D → A.IsFacet (Finset.image f F) (Finset.image f D)) ∧ (∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (D : Finset V), cc.IsMaximal D → Finset.image f D = D → ∃! D' : Finset V, cc.IsMaximal D' ∧ D' ≠ D ∧ Finset.image f D' = D) ∧ ∀ (cc : ChamberComplex V), cc.toSimplicialComplex = A → ∀ (A₀ B : Finset V), cc.IsMaximal A₀ → Finset.image f A₀ = A₀ → cc.IsMaximal B → Finset.image f B = B → ∀ (g : Gallery cc.toSimplicialComplex), g.Connects A₀ B → g.length = galleryDist cc.toSimplicialComplex A₀ B → ∀ (Ci Ci1 : Finset V), Ci ∈ g.chambers → Ci1 ∈ g.chambers → cc.Adjacent Ci Ci1 → Finset.image f Ci1 = Finset.image f Ci → False

For adjacent chambers $C, C'$, there is a vertex map fixing $C$ and sending the third chamber containing the panel to $C'$ (used to construct foldings from thickness).

theorem ThicknessFoldings.folding_from_simplicial_map {V : Type} [DecidableEq V] (cc : ChamberComplex V) (hthin : cc.IsThin) (f : V → V) (hface : ∀ s ∈ cc.faces, Finset.image f s ∈ cc.faces) (hidempotent : ∀ (v : V), f (f v) = f v) (hchamberMap : ∀ (D : Finset V), cc.IsMaximal D → cc.IsMaximal (Finset.image f D)) (hpreservesFacets : ∀ (F D : Finset V), cc.IsFacet F D → cc.IsFacet (Finset.image f F) (Finset.image f D)) (htwoToOne : ∀ (D : Finset V), cc.IsMaximal D → Finset.image f D = D → ∃! D' : Finset V, cc.IsMaximal D' ∧ D' ≠ D ∧ Finset.image f D' = D) (hstutter_contradicts_minimality : ∀ (A B : Finset V), cc.IsMaximal A → Finset.image f A = A → cc.IsMaximal B → Finset.image f B = B → ∀ (g : Gallery cc.toSimplicialComplex), g.Connects A B → g.length = galleryDist cc.toSimplicialComplex A B → ∀ (Ci Ci1 : Finset V), Ci ∈ g.chambers → Ci1 ∈ g.chambers → cc.Adjacent Ci Ci1 → Finset.image f Ci1 = Finset.image f Ci → False) (C C' : Finset V) (hadj : cc.Adjacent C C') (hfC : Finset.image f C = C) (hfC' : Finset.image f C' = C) : ∃ (fold : cc.Folding), Finset.image fold.morph.toFun C = C ∧ Finset.image fold.morph.toFun C' = C

Construct a folding from a simplicial map fixing a chamber and sending its panel-mate to itself — the third-chamber map of a thick complex.

theorem ThicknessFoldings.apt_has_sufficient_foldings {V : Type} [DecidableEq V] (K : ChamberComplex V) (hK_thick : K.IsThick) (pre : AptIsCoxeterProof.PreApartmentData K) (A : SimplicialComplex V) (hA : A ∈ pre.apartments) (cc : ChamberComplex V) (hcc_eq : cc.toSimplicialComplex = A) (hcc_thin : cc.IsThin) : AptIsCoxeterProof.HasSufficientFoldings cc

Every apartment of a thick chamber complex has sufficient foldings (every adjacent pair is collapsed by some folding).

theorem ThicknessFoldings.thickness_implies_apt_structure_hyp {V : Type} [DecidableEq V] : AptIsCoxeterProof.ThicknessImpliesAptStructureHyp V

Main theorem: thickness of a chamber complex implies that every apartment has sufficient foldings — discharging the ThicknessImpliesAptStructureHyp.