The Morley–Hanf theorem, discharged

The honest residual MorleySeedTailTemplateRealizable — the sole non-formal input of the realizability-only Morley–Hanf endpoint morley_hanf_of_tail_realizable — is PROVED by the schema route (morleySeed_tailTemplate_model_of_schemaSource): the ω-stage Marker/Henkin completion of the schema sentence universe, its quotient term model with the restricted truth lemma, the fully indiscernible sequence schemaSeq with pinned iSup/negative-iInf witnesses, and the cross-source acceptance through the Skolem-universality mixin. In fact the schema route consumes strictly LESS than the residual offers: the input sequence's tail indiscernibility is not used (seed template values are absolute).

morley_hanf_countable_symbols is the transparent countable-symbol intermediate. The definitive endpoint morley_hanf carries NO symbol-countability hypotheses: the construction runs in the simultaneous symbol-generated sublanguage of φ (symbSublang φ.functionsIn φ.relationsIn, both sorts countable because a formula mentions countably many symbols), and the resulting model is expanded back to L'[[J]] — missing functions act arbitrarily, missing relations as False, constants pass through; the degenerate IsEmpty J case is served by the source model itself. So: ℶ_{ω₁} is a Hanf bound for every L_{ω₁ω} sentence, unconditionally.

Removing symbol countability: the two-sorted sublanguage reduction

@[reducible]

noncomputable def FirstOrder.Language.expandSymbStructure {L : Language} (F : Set ((n : ℕ) × L.Functions n)) (R : Set ((n : ℕ) × L.Relations n)) (J : Type) {N : Type} [Nonempty N] [instN : ((symbSublang F R).withConstants J).Structure N] : (L.withConstants J).Structure N

Expansion of a two-sorted sublanguage [[J]]-structure to the full language: generating function symbols act as before, missing functions act arbitrarily (hence [Nonempty N]); generating relation symbols act as before, missing relations are False; constants pass through.

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.morleySeedTailTemplateRealizable_holds {L' : Language} : MorleySeedTailTemplateRealizable

The honest Morley–Hanf residual holds — no symbol-countability assumptions: the schema construction runs in the simultaneous symbol-generated sublanguage of φ (both sorts countable, proved not assumed) at an injective ℕ-sequence of the source, and its model expands back to L'[[J]]; the degenerate IsEmpty J case is served by the source model itself.

theorem FirstOrder.Language.morley_hanf {L' : Language} (φ : L'.Sentenceω) : IsHanfBound φ (Cardinal.beth (Ordinal.omega 1))

The Morley–Hanf theorem: ℶ_{ω₁} is a Hanf bound for every L_{ω₁ω} sentence — over an arbitrary language, with no countability or other side hypotheses. If an L_{ω₁ω} sentence has a model of size at least ℶ_{ω₁}, it has models of arbitrarily large cardinality.