noncomputable def buildingAtInfinity_full {V : Type} [DecidableEq V] (b : Building V) (si : AffineBuilding.SectorInfrastructure b) (md : AffineBuilding.ApartmentMetricData b) (h_nonempty : b.apartmentSystem.apartments.Nonempty) : AffineBuilding.SphericalSimplicialComplex b md

Bundles the spherical building at infinity $X_\infty$ together with its simplicial complex structure: assembles the boundary $|X_\infty|$ from sectors, verifying both sphericality and the simplicial-complex axioms (Sections 16.8–16.10).