The ω₁ cofinal-fiber engine (issue #12, risky engine 1)

A countable partition of ω₁ has an unbounded fiber: any assignment of countably many labels to the countable ordinals takes some label unboundedly often below ω₁.

This is the single reusable pigeonhole behind every branching closure field of the well-ordering consistency property — implication branching, positive disjunctions, and negated conjunctions alike (audit v2, C4 engine): each α < ω₁ chooses a branch, some branch recurs unboundedly, and downward closure of the gap witness (GapWitness.mono) upgrades "unboundedly many α" to "all α".

Proof: if every fiber were bounded, the supremum of countably many bounds would bound all of ω₁ — contradicting the regularity of ℵ₁ (via Ordinal.iSup_lt_omega_one).

theorem FirstOrder.Language.exists_unbounded_fiber {ι : Type} [Countable ι] [Nonempty ι] (f : Ordinal.{0} → ι) : ∃ (i : ι), ∀ β < (Cardinal.aleph 1).ord, ∃ (α : Ordinal.{0}), β ≤ α ∧ α < (Cardinal.aleph 1).ord ∧ f α = i

The cofinal-fiber lemma: a countably-labelled assignment on the ordinals takes some label unboundedly often below ω₁ = (Cardinal.aleph 1).ord.