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

Hypothesis: a panel compatible with a frame $F$ admits two distinct frame-compatible subspaces $W_1, W_2$, each extending the panel into a chamber.

• fill_gap (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)), W₁ ≠ W₂ ∧ Frame.IsCompatible k n F W₁ ∧ Frame.IsCompatible k n F W₂ ∧ (∃ (C₁ : SubspaceFlag k n), IsChamber k n C₁ ∧ (∀ V ∈ panel.chain, V ∈ C₁.chain) ∧ W₁ ∈ C₁.chain) ∧ ∃ (C₂ : SubspaceFlag k n), IsChamber k n C₂ ∧ (∀ V ∈ panel.chain, V ∈ C₂.chain) ∧ W₂ ∈ C₂.chain

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

Hypothesis: a panel compatible with a frame extends directly to two distinct chambers, both containing every subspace of the panel.

• extend (F : Frame k n) (panel : SubspaceFlag k n) : (∀ V ∈ panel.chain, Frame.IsCompatible k n F V) → panel.chain.length = n - 2 → ∃ (C₁ : SubspaceFlag k n) (C₂ : SubspaceFlag k n), IsChamber k n C₁ ∧ IsChamber k n C₂ ∧ C₁ ≠ C₂ ∧ (∀ V ∈ panel.chain, V ∈ C₁.chain) ∧ ∀ V ∈ panel.chain, V ∈ C₂.chain

noncomputable def GLnBuilding.panelExtensionOfDirect (k : Type u_1) [Field k] (n : ℕ) (h : DirectPanelExtensionHyp k n) : PanelExtensionHyp k n

Wrapper turning a DirectPanelExtensionHyp into a PanelExtensionHyp.