theorem GLnBuilding.insertIdx_eq_take_append_drop' {α : Type u_2} {l : List α} {w : α} {i : ℕ} (hi : i ≤ l.length) : l.insertIdx i w = List.take i l ++ w :: List.drop i l

List.insertIdx decomposed as take ++ a :: drop.

theorem GLnBuilding.pairwise_insertIdx_of_pairwise {α : Type u_2} {R : α → α → Prop} {l : List α} {w : α} {i : ℕ} (hpw : List.Pairwise R l) (hi : i ≤ l.length) (hbefore : ∀ x ∈ List.take i l, R x w) (hafter : ∀ y ∈ List.drop i l, R w y) : List.Pairwise R (l.insertIdx i w)

Inserting an element at index $i$ preserves Pairwise R, given the appropriate relation to elements before and after position $i$.

theorem GLnBuilding.isChain_insertIdx_of_isChain {α : Type u_2} {R : α → α → Prop} [Trans R R R] {l : List α} {w : α} {i : ℕ} (hch : List.IsChain R l) (hi : i ≤ l.length) (hbefore : ∀ x ∈ List.take i l, R x w) (hafter : ∀ y ∈ List.drop i l, R w y) : List.IsChain R (l.insertIdx i w)

Inserting an element preserves the IsChain R property under the same conditions.

structure GLnBuilding.PanelGapHyp (k : Type u_1) [Field k] (n : ℕ) : Prop

Hypothesis: a panel (length $n-2$ chain) compatible with a frame can be extended to two distinct chambers, both containing the panel.

• fill_gap (F : Frame k n) (panel : SubspaceFlag k n) : (∀ V ∈ panel.chain, Frame.IsCompatible k n F V) → panel.chain.length = n - 2 → ∃ (chain₁ : List (Submodule k (Vec k n))) (chain₂ : List (Submodule k (Vec k n))), chain₁ ≠ [] ∧ List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain₁ ∧ (∀ V ∈ chain₁, V ≠ ⊥ ∧ V ≠ ⊤) ∧ chain₁.length = n - 1 ∧ chain₂ ≠ [] ∧ List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain₂ ∧ (∀ V ∈ chain₂, V ≠ ⊥ ∧ V ≠ ⊤) ∧ chain₂.length = n - 1 ∧ (∀ V ∈ panel.chain, V ∈ chain₁) ∧ (∀ V ∈ panel.chain, V ∈ chain₂) ∧ chain₁ ≠ chain₂

structure GLnBuilding.FrameGapFillerHyp (k : Type u_1) [Field k] (n : ℕ) : Prop

Hypothesis: given a panel and a compatible frame, one can produce two distinct subspaces $W_1, W_2$ that, when inserted at a common position, each turn the panel into a chamber.

• find_and_fill (F : Frame k n) (panel : SubspaceFlag k n) : (∀ V ∈ panel.chain, Frame.IsCompatible k n F V) → panel.chain.length = n - 2 → ∃ (W₁ : Submodule k (Vec k n)) (W₂ : Submodule k (Vec k n)) (pos : ℕ), W₁ ≠ W₂ ∧ W₁ ≠ ⊥ ∧ W₁ ≠ ⊤ ∧ W₂ ≠ ⊥ ∧ W₂ ≠ ⊤ ∧ pos ≤ panel.chain.length ∧ List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) (panel.chain.insertIdx pos W₁) ∧ (panel.chain.insertIdx pos W₁).length = n - 1 ∧ List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) (panel.chain.insertIdx pos W₂) ∧ (panel.chain.insertIdx pos W₂).length = n - 1 ∧ (∀ V ∈ panel.chain.insertIdx pos W₁, V ≠ ⊥ ∧ V ≠ ⊤) ∧ ∀ V ∈ panel.chain.insertIdx pos W₂, V ≠ ⊥ ∧ V ≠ ⊤

structure GLnBuilding.SubmoduleGapInsertionHyp (k : Type u_1) [Field k] (n : ℕ) : Prop

Hypothesis: any length-$(n-2)$ chain admits two distinct frame-compatible insertions $W_1, W_2$ at a common index, sandwiched strictly between the surrounding terms.

• find_gap (F : Frame k n) (chain : List (Submodule k (Vec k n))) : List.IsChain (fun (x1 x2 : Submodule k (Vec k n)) => x1 < x2) chain → (∀ V ∈ chain, Frame.IsCompatible k n F V) → (∀ V ∈ chain, V ≠ ⊥ ∧ V ≠ ⊤) → chain.length = n - 2 → ∃ (W₁ : Submodule k (Vec k n)) (W₂ : Submodule k (Vec k n)) (pos : ℕ), W₁ ≠ W₂ ∧ W₁ ≠ ⊥ ∧ W₁ ≠ ⊤ ∧ W₂ ≠ ⊥ ∧ W₂ ≠ ⊤ ∧ pos ≤ chain.length ∧ (∀ x ∈ List.take pos chain, x < W₁) ∧ (∀ y ∈ List.drop pos chain, W₁ < y) ∧ (∀ x ∈ List.take pos chain, x < W₂) ∧ ∀ y ∈ List.drop pos chain, W₂ < y

structure GLnBuilding.FrameFinsetCorrespondenceHyp (k : Type u_1) [Field k] (n : ℕ) : Type u_1

Hypothesis bundling the bijective correspondence between $F$-compatible subspaces of $k^n$ and subsets $S \subseteq \{1,\dots,n\}$ via $S \mapsto \bigoplus_{i \in S} L_i$; this records the extraction, its inverse, strict-monotonicity, and properness preservation.

• extract : Frame k n → Submodule k (Vec k n) → Finset (Fin n)
• extract_eq (F : Frame k n) (V : Submodule k (Vec k n)) : Frame.IsCompatible k n F V → V = ⨆ i ∈ self.extract F V, F.lines i
• extract_ssubset (F : Frame k n) (V₁ V₂ : Submodule k (Vec k n)) : Frame.IsCompatible k n F V₁ → Frame.IsCompatible k n F V₂ → V₁ < V₂ → self.extract F V₁ ⊂ self.extract F V₂
• extract_nonempty (F : Frame k n) (V : Submodule k (Vec k n)) : Frame.IsCompatible k n F V → V ≠ ⊥ → (self.extract F V).Nonempty
• extract_proper (F : Frame k n) (V : Submodule k (Vec k n)) : Frame.IsCompatible k n F V → V ≠ ⊤ → self.extract F V ≠ Finset.univ
• lift_ssubset (F : Frame k n) (S₁ S₂ : Finset (Fin n)) : S₁ ⊂ S₂ → ⨆ i ∈ S₁, F.lines i < ⨆ i ∈ S₂, F.lines i
• lift_nonempty (F : Frame k n) (S : Finset (Fin n)) : S.Nonempty → ⨆ i ∈ S, F.lines i ≠ ⊥
• lift_proper (F : Frame k n) (S : Finset (Fin n)) : S ≠ Finset.univ → ⨆ i ∈ S, F.lines i ≠ ⊤
• lift_ne (F : Frame k n) (S₁ S₂ : Finset (Fin n)) : S₁ ≠ S₂ → ⨆ i ∈ S₁, F.lines i ≠ ⨆ i ∈ S₂, F.lines i

structure GLnBuilding.FinsetChainGapHyp (n : ℕ) : Prop

Hypothesis: any strictly increasing chain of proper non-empty subsets of $\mathrm{Fin}\ n$ of length $n-2$ admits two distinct insertions at a common position.

• find_gap (chain : List (Finset (Fin n))) : List.IsChain (fun (x1 x2 : Finset (Fin n)) => x1 ⊂ x2) chain → (∀ S ∈ chain, S.Nonempty) → (∀ S ∈ chain, S ≠ Finset.univ) → chain.length = n - 2 → ∃ (T₁ : Finset (Fin n)) (T₂ : Finset (Fin n)) (pos : ℕ), T₁ ≠ T₂ ∧ T₁.Nonempty ∧ T₁ ≠ Finset.univ ∧ T₂.Nonempty ∧ T₂ ≠ Finset.univ ∧ pos ≤ chain.length ∧ (∀ S ∈ List.take pos chain, S ⊂ T₁) ∧ (∀ S ∈ List.drop pos chain, T₁ ⊂ S) ∧ (∀ S ∈ List.take pos chain, S ⊂ T₂) ∧ ∀ S ∈ List.drop pos chain, T₂ ⊂ S

noncomputable def GLnBuilding.submoduleGapInsertionOfSubHyps (k : Type u_1) [Field k] (n : ℕ) (hcorr : FrameFinsetCorrespondenceHyp k n) (hgap_finset : FinsetChainGapHyp n) : SubmoduleGapInsertionHyp k n

Lift the finset gap-insertion property to the submodule level via the frame-finset correspondence, transporting the two distinct insertions along $S \mapsto \bigoplus_{i \in S} L_i$.

noncomputable def GLnBuilding.frameGapFillerOfGapInsertion (k : Type u_1) [Field k] (n : ℕ) (hgap : SubmoduleGapInsertionHyp k n) : FrameGapFillerHyp k n

Convert a submodule gap-insertion into a frame gap filler: the two distinct insertions literally produce two distinct chambers via insertIdx.

theorem GLnBuilding.insertIdx_ne_of_ne {α : Type u_2} {l : List α} {a b : α} {i : ℕ} (hne : a ≠ b) (hi : i ≤ l.length) : l.insertIdx i a ≠ l.insertIdx i b

Inserting two different elements at the same position yields different lists.

noncomputable def GLnBuilding.panelGapOfFrameGapFiller (k : Type u_1) [Field k] (n : ℕ) (filler : FrameGapFillerHyp k n) : PanelGapHyp k n

Wrap a FrameGapFillerHyp into a PanelGapHyp by reading off the two distinct extended chambers obtained from the insertions $W_1 \ne W_2$.

noncomputable def GLnBuilding.directPanelExtensionOfGap (k : Type u_1) [Field k] (n : ℕ) (gap : PanelGapHyp k n) : DirectPanelExtensionHyp k n

Convert a PanelGapHyp into a DirectPanelExtensionHyp by packaging the two chains as SubspaceFlags with the chamber property.