noncomputable def GLnBuilding.thinApartmentHypComposed (k : Type u_1) [Field k] (n : ℕ) (hn2 : 2 ≤ n) : ThinApartmentHyp k n

Cascade of constructions assembling the thin-apartment property unconditionally for $n \ge 2$: from the finset gap and frame–finset correspondence, derive a submodule gap insertion, then a frame gap filler, then a panel-gap, a direct panel extension, and finally the full ThinApartmentHyp.