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 by2 ^ ·: the successor-level case (with Mathlib'sCardinal.beth_succfor 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.
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.
A countable dependent sum of types each of size ≤ κ has size ≤ κ, for infinite κ.
A countable union of sets each of size ≤ κ has size ≤ κ, for infinite κ — the
limit-level case of the ladder induction.
An injection into a powerset bounds by 2 ^ · — the successor-level case of the ladder
induction.
The successor-cofinal supremum at ω₁: ⨆_{α<ω₁} ℶ_{α+1} = ℶ_{ω₁} — the ladder's
endpoint.