Compact-Range Vietoris Powers of Countable Ordinals

For every ordinal ω < α < ω1, the ordered compact-set space K(α, ord) of Caruvana andHolshouser is second-countable and Lindelo¨f, but neither σ-compact nor Menger. This answersQuestion 2.18 of their published paper. We first prove that a second-countable ground space has asecond-countable compact-range Vietoris power at countable index. A delayed diagonal then showsthat the closed family of surjections onto ω + 1 with zeroth coordinate ω is not σ-compact. Closedinclusions induce closed embeddings at a fixed index, so this obstruction transfers to every ordinal inthe stated interval. Explicit coordinate covers yield the non-Menger conclusion. The proofs areself-contained, consolidate the earlier convergent-sequence case with its generalization, and areaccompanied by a Lean 4 formalization of the principal ordinal theorem.