Bounded capture for the separation-width hierarchy

The hierarchy uses the direct diagonal construction from Simplified.Capture. These compatibility theorems keep the width API without maintaining a second finite-state construction and a separate induction on the cardinality bound.

theorem GenLimit.FiniteWitness.bounded_capture {α : Type u_1} (d : ℕ) (U : ℕ → Finset α) (hU : ∀ (n : ℕ), (U n).card ≤ d) (C : ℕ → Set α) : ∃ (D : Set α), {n : ℕ | ↑(U n) ⊆ D}.Infinite ∧ ∀ (m : ℕ), (C m).Infinite → ¬C m ⊆ D

A uniformly bounded finite-set sequence is captured infinitely often by one set containing none of the prescribed infinite cores. The universe is arbitrary; no countability or measurability of its points is assumed.

theorem GenLimit.FiniteWitness.bounded_capture_indexed {α : Type u_1} {ι : Type u_2} [Countable ι] (d : ℕ) (U : ℕ → Finset α) (hU : ∀ (n : ℕ), (U n).card ≤ d) (C : ι → Set α) : ∃ (D : Set α), {n : ℕ | ↑(U n) ⊆ D}.Infinite ∧ ∀ (i : ι), (C i).Infinite → ¬C i ⊆ D