The beth ladder: sharpness of the Morley–Hanf bound

The assembly of Marker's Exercise 5.3 ladder: for every α < ω₁ the ladder sentence has the von Neumann model of size exactly ℶ_{α+1} (VonNeumannModel.lean) and no larger models (LadderBound.lean), so through the generic bounded-spectrum endpoint each ℶ_{α+1} is a strict lower bound for the global Hanf number; the successor-cofinal supremum (CardinalBounds.lean) then gives ℶ_{ω₁} ≤ Hanf(L_{ω₁ω}). Combined with the Morley–Hanf upper bound Lomega1omegaHanfNumber_le_beth_omega1:

• Lomega1omegaHanfNumber_eq_beth_omega1 — Hanf(L_{ω₁ω}) = ℶ_{ω₁}, the exact Hanf number of L_{ω₁ω} over Language.{0,0}.

Reference: Marker, Lectures on Infinitary Model Theory, Exercise 5.3 and Theorem 5.4.

theorem FirstOrder.Language.beth_add_one_lt_Lomega1omegaHanfNumber {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) : Cardinal.beth (α + 1) < Lomega1omegaHanfNumber

The per-stage sharpness step: for every α < ω₁, the ladder sentence has maximal model size exactly ℶ_{α+1}, so ℶ_{α+1} < Lomega1omegaHanfNumber.

theorem FirstOrder.Language.beth_omega1_le_Lomega1omegaHanfNumber : Cardinal.beth (Ordinal.omega 1) ≤ Lomega1omegaHanfNumber

The lower half of the Hanf-number computation: ℶ_{ω₁} ≤ Lomega1omegaHanfNumber, by the successor-cofinal supremum over the ladder stages.

theorem FirstOrder.Language.Lomega1omegaHanfNumber_eq_beth_omega1 : Lomega1omegaHanfNumber = Cardinal.beth (Ordinal.omega 1)

The Hanf number of L_{ω₁ω} is exactly ℶ_{ω₁} (Morley; Marker, Theorem 5.4): the Morley–Hanf upper bound morley_hanf is sharp.