Cardinal lemmas for the beth ladder

The consumer-shaped cardinal arithmetic of the Hanf beth-ladder upper-bound induction and its supremum endpoint (docs/hanf-ladder-audit.md §3, §5) — no syntax, no models:

• mk_sigma_le_of_countable / mk_iUnion_le_of_countable — countable families of ≤ κ-sized pieces stay ≤ κ (for infinite κ): the limit-level case;
• sum_le_of_countable_lift / lift_mk_iUnion_le_of_countable — the same, for a bound that does not live in the ambient universe. A bound assembled from both language data and structure data is in neither, so the same-universe forms cannot state it;
• mk_le_two_power_of_injective_set — an injection into a powerset bounds by 2 ^ ·: the successor-level case (with Mathlib's Cardinal.beth_succ for orientation);
• iSup_beth_add_one_omega1 — the successor-cofinal supremum at ω₁: ⨆_{α<ω₁} ℶ_{α+1} = ℶ_{ω₁} — the endpoint that turns the per-stage witnesses into ℶ_{ω₁} ≤ Hanf(L_{ω₁ω}).

Marker's recursion ℶ_α = sup_{β<α} 2^{ℶ_β} agrees with Mathlib's beth for α ≠ 0 (at 0 the right side is the empty supremum), so Mathlib's beth_zero/beth_succ/beth_limit are used directly as the formal interface; no second recursive beth is introduced.

theorem FirstOrder.HanfLadder.sum_le_of_countable {ι : Type u} [Countable ι] {f : ι → Cardinal.{u}} {κ : Cardinal.{u}} (hκ : Cardinal.aleph0 ≤ κ) (hf : ∀ (i : ι), f i ≤ κ) : Cardinal.sum f ≤ κ

The countable-sum core: a countable sum of cardinals each ≤ κ is ≤ κ, for infinite κ.

theorem FirstOrder.HanfLadder.sum_le_of_countable_lift {ι : Type u} [Countable ι] {f : ι → Cardinal.{v}} {κ : Cardinal.{max u v}} (hκ : Cardinal.aleph0 ≤ κ) (hf : ∀ (i : ι), Cardinal.lift.{u, v} (f i) ≤ κ) : Cardinal.sum f ≤ κ

sum_le_of_countable with the bound in a larger universe than the index type.

A bound assembled from both language data and structure data does not live in the structure's universe, so the same-universe form cannot state it. The index type still has to be countable in its own universe; only the summands move.

theorem FirstOrder.HanfLadder.lift_mk_iUnion_le_of_countable {M : Type u} {ι : Type w} [Countable ι] {X : ι → Set M} {κ : Cardinal.{max u v w}} (hκ : Cardinal.aleph0 ≤ κ) (hX : ∀ (i : ι), Cardinal.lift.{max v w, u} (Cardinal.mk ↑(X i)) ≤ κ) : Cardinal.lift.{max v w, u} (Cardinal.mk ↑(⋃ (i : ι), X i)) ≤ κ

The lifted form of mk_iUnion_le_of_countable, for a bound outside the ambient universe.

The index type gets its own universe: an index fixed independently of the ambient type (a stage count, say) would otherwise drag that type down to the index's universe.

theorem FirstOrder.HanfLadder.mk_sigma_le_of_countable {ι : Type u} [Countable ι] {X : ι → Type u} {κ : Cardinal.{u}} (hκ : Cardinal.aleph0 ≤ κ) (hX : ∀ (i : ι), Cardinal.mk (X i) ≤ κ) : Cardinal.mk ((i : ι) × X i) ≤ κ

A countable dependent sum of types each of size ≤ κ has size ≤ κ, for infinite κ.

theorem FirstOrder.HanfLadder.mk_iUnion_le_of_countable {M ι : Type u} [Countable ι] {X : ι → Set M} {κ : Cardinal.{u}} (hκ : Cardinal.aleph0 ≤ κ) (hX : ∀ (i : ι), Cardinal.mk ↑(X i) ≤ κ) : Cardinal.mk ↑(⋃ (i : ι), X i) ≤ κ

A countable union of sets each of size ≤ κ has size ≤ κ, for infinite κ — the limit-level case of the ladder induction.

theorem FirstOrder.HanfLadder.mk_le_two_power_of_injective_set {X Y : Type u} {f : X → Set Y} (hf : Function.Injective f) : Cardinal.mk X ≤ 2 ^ Cardinal.mk Y

An injection into a powerset bounds by 2 ^ · — the successor-level case of the ladder induction.

theorem FirstOrder.HanfLadder.iSup_beth_add_one_omega1 : ⨆ (α : ↑(Set.Iio (Ordinal.omega 1))), Cardinal.beth (↑α + 1) = Cardinal.beth (Ordinal.omega 1)

The successor-cofinal supremum at ω₁: ⨆_{α<ω₁} ℶ_{α+1} = ℶ_{ω₁} — the ladder's endpoint.