Morley-Hanf Transfer Hypothesis (Conditional)

This file isolates the deep combinatorial transfer hypothesis needed for the Morley-Hanf theorem. The hypothesis encapsulates Erdős-Rado extraction + Ehrenfeucht-Mostowski stretching, which require infrastructure not currently formalized in Lean or Mathlib.

Conditional Status

MorleyHanfTransfer is a Prop-valued definition, not a theorem. The conditional theorem morley_hanf_of_transfer takes it as a hypothesis. Both are placed in Conditional/ to make the external dependency visible.

References

• [Mar16], §5
• [KK04], §1.6

def FirstOrder.Language.MorleyHanfTransfer (L : Language) [Countable ((l : ℕ) × L.Relations l)] : Prop

Deep set-theoretic/model-theoretic transfer hypothesis for the Morley-Hanf theorem.

This encapsulates the combined content of:

1. Erdős-Rado extraction: Models of size ≥ ℶ_{ω₁} in a countable language contain Lω₁ω-indiscernible sequences of uncountable length.
2. Ehrenfeucht-Mostowski stretching: Such indiscernible sequences can be stretched to produce models of arbitrary size satisfying the same Lω₁ω sentences.

These deep combinatorial arguments (Ramsey/partition calculus + EM functors) require infrastructure not currently formalized in Lean or Mathlib.

See [Mar16], §5; [KK04], §1.6.

Equations

• L.MorleyHanfTransfer = ∀ (φ : L.Sentenceω) (M : Type) [inst : L.Structure M], φ.Realize M → Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1) → FirstOrder.Language.HasArbLargeModels φ

theorem FirstOrder.Language.morley_hanf_of_transfer {L : Language} [Countable ((l : ℕ) × L.Relations l)] (htransfer : L.MorleyHanfTransfer) (φ : L.Sentenceω) : IsHanfBound φ (Cardinal.beth (Ordinal.omega 1))

Morley-Hanf Theorem (historical form, conditional on the transfer hypothesis).

For a countable language, the Hanf number of any Lω₁ω sentence is bounded by ℶ_ω₁ (the ω₁-th beth number), assuming the deep combinatorial transfer principle MorleyHanfTransfer.

Superseded: the unconditional theorem is morley_hanf (Conditional/MorleyHanfSchemaDischarge.lean), with no hypotheses at all — the transfer content was discharged by the tail extraction (morleyHanfExtractionTail_holds) plus the schema-route seed-template realizability (morleySeedTailTemplateRealizable_holds). This form is retained as the historical statement shape.

Residual extraction hypothesis + proved bridge

Phase 2 refactor: split MorleyHanfTransfer into a source-side extraction hypothesis (still conditional) plus a compactness oracle, joined by a proved bridge theorem. The extraction is the genuine combinatorial residual (Erdős–Rado + pairwise-distinct stable-type extraction); the stretching side is now fully formalized in Methods/EM/FragmentAdapter.lean.

Universe note: the bridge uses L : Language.{0, 0} so that the target linear order J : Type (produced via (Cardinal.ord κ).ToType at Cardinal.{0}) matches the universe expected by the stretching theorems (which take {J : Type u} tied to L's first universe).

def FirstOrder.Language.MorleyHanfExtraction {L' : Language} : Prop

Residual source-side extraction hypothesis.

From a model of size ≥ ℶ_ω₁ in a countable-relational language, extract a pairwise-distinct ℕ-indexed sequence that is restricted-indiscernible on any chosen countable formula family s.

This is the genuine combinatorial content left after separating out EM stretching: Erdős–Rado-style partition arguments for Lω₁ω plus a stable-type extraction. The sequence does NOT need to have an uncountable index set — Phase 1's arbitrary-J stretching means a countable source suffices.

FALSE-SHAPED (statement audit 2026-07-07). Refutable in ZFC: over an arbitrary countable relational L', every Bool coloring of increasing n-tuples of a well-ordered carrier is definable (one n-ary relation symbol per coloring), and an increasing subsequence of the extracted pairwise-distinct sequence exists by well-foundedness — so this hypothesis implies the failed partition relation ℶ_ω₁ → (ω)^{<ω}_2; see the full Erdős-cardinal argument on PureColoringHypothesis below. Full ω-sequence indiscernibility on a countable family never lives in the SOURCE model; classically it appears only in the model built from the EM template by Model Existence [Marker §5.2]. Kept as the consumer interface of the local EM route (morley_hanf_of_morleyHanfExtraction remains a true implication).

Equations

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

theorem FirstOrder.Language.hasArbLargeModels_of_restricted_extraction {L' : Language} (hExtract : MorleyHanfExtraction) (hCompact : ∀ (J : Type) [LinearOrder J] (S : Set (L'.withConstants J).Sentenceω), (∀ (F : Set (L'.withConstants J).Sentenceω), F.Finite → F ⊆ S → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model F N) → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model S N) (φ : L'.Sentenceω) (hφ : ∃ (M : Type) (x : L'.Structure M), φ.Realize M ∧ Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1)) : HasArbLargeModels φ

Morley–Hanf via restricted extraction + compactness (proved).

Assuming the residual extraction hypothesis MorleyHanfExtraction L and a per-target compactness oracle for every L[[J]], any sentence realized in a model of size ≥ ℶ_ω₁ has arbitrarily large models.

The proof combines:

• hExtract to obtain a pairwise-distinct ℕ-indexed sequence that is restricted-indiscernible on {⟨0, φ⟩, ⟨2, disEqFormula⟩},
• stretch_restricted_sequence_of_compact (tranche 2b) to stretch the sequence into a target model N over an arbitrarily large J,
• inline derivations of (a) sentence preservation from the empty-tuple application of the stretching equivalence, and (b) injectivity of b : J → N from the pair-tuple application.

Tail-weakened residual

The interface-refinement audit (2026-06-10) showed that the EM stretching pipeline consumes source-side indiscernibility only through the finite-satisfiability lemma, where the interpreting tuple is freely chosen — so per-formula tail indiscernibility suffices (see Methods/EM/TailAdapter.lean). The tail residual below matches what classical Erdős–Rado extraction actually produces in the source model (per-arity cutoffs, no full simultaneity across arities), and is implied by the original MorleyHanfExtraction.

def FirstOrder.Language.MorleyHanfExtractionTail {L' : Language} : Prop

Tail-weakened residual extraction hypothesis. Like MorleyHanfExtraction, but the extracted sequence is only required to be tail-indiscernible on the family: for each formula there is a cutoff beyond which all strictly monotone tuples agree. This is the form a per-arity Erdős–Rado schedule produces.

Equations

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

theorem FirstOrder.Language.morleyHanfExtractionTail_holds {L' : Language} : MorleyHanfExtractionTail

MorleyHanfExtractionTail holds (cheap route, modulo infinite_ramsey_nat_family).

The tail residual is dischargeable from a merely countably-infinite source — the ℶ_{ω₁} hypothesis is not consumed. Because the colorings are Bool-per-formula and the tail cutoff is per-formula, the extraction is an infinite Ramsey fact on ℕ, not an Erdős–Rado/beth-schedule theorem:

• take an injective a : ℕ → M (Infinite.natEmbedding; no order on M is needed — the formula realization ignores it, the "increasing tuple" structure lives entirely in the ℕ index);
• pull each formula's truth back to a Bool coloring of strictly-increasing ℕ-tuples;
• apply the countable-family diagonal Ramsey theorem infinite_ramsey_nat_family to obtain a single g : ℕ ↪o ℕ that is eventually homogeneous for every coloring;
• read off pairwise-distinctness (injectivity) and per-formula tail indiscernibility of a ∘ g.

The ℶ_{ω₁} beth schedule is a strictly stronger statement (full/uncountable indiscernibility), not required by this bridge.

theorem FirstOrder.Language.morleyHanfExtractionTail_of_morleyHanfExtraction {L' : Language} (h : MorleyHanfExtraction) : MorleyHanfExtractionTail

The original (full-indiscernibility) residual implies the tail residual.

def FirstOrder.Language.TailTemplateRealizable {L' : Language} : Prop

The broad tail-template residual — WARNING: false-shaped over arbitrary sequences. Quantifying over every formula sequence s makes this a genuine L_{ω₁ω} compactness statement, refutable: over a language with unary predicates Pᵢ, take a "height" model (Pᵢ x ↔ i ≤ height x, heights unbounded, model as large as desired), a n of height n, and s enumerating every Pᵢ x together with ⋀ᵢ Pᵢ x. Then a is tail-indiscernible on Set.range s (each Pᵢ (a n) is eventually true; ⋀ᵢ Pᵢ (a n) is constantly false), and the tail-template theory contains every positive Pᵢ (c_j) and also ¬⋀ᵢ Pᵢ (c_j) — finitely satisfiable but unsatisfiable. The ℶ_{ω₁} premise does not help: the red flag is precisely a bridge that consumes it only to make M nonempty.

The honest residual is MorleySeedTailTemplateRealizable below, quantified only over the Morley seed {φ, x₀ ≠ x₁} actually fed to the bridge, and carrying the source facts actually available (φ holds in the large M, the sequence is pairwise distinct). This broad form is retained only as the compactness-strength marker witnessed by tailTemplateRealizable_of_compact; nothing should aim to prove it — it is now formally refuted: T_counterexample (end of this file) instantiates the height-model counterexample at the concrete language HeightCex.Lang.

Equations

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

def FirstOrder.Language.MorleySeedTailTemplateRealizable {L' : Language} : Prop

The honest residual consumed by the tail Morley–Hanf bridge: realizability of the tail-template theory of the Morley seed {φ, x₀ ≠ x₁} only, carrying the source facts the bridge actually has — φ holds in the source model M of size ≥ ℶ_{ω₁}, and the extracted sequence is pairwise distinct and tail-indiscernible on the seed.

The |M| ≥ ℶ_ω₁ premise is essential for the statement to be true-shaped: the seed's template theory is {φ} ∪ {distinct constants}, so realizability over a size-κ order is "φ has a model of size ≥ κ" — without the cardinality premise this would assert that every φ with an infinite model has arbitrarily large models, false for Scott sentences of bounded Hanf number. Unlike the broad TailTemplateRealizable (false-shaped: see its docstring), the seed family has no countable connectives beyond those inside φ itself, and the classical proof is the Ehrenfeucht–Mostowski / Skolem-hull construction over J.

Now PROVED (morleySeedTailTemplateRealizable_holds, Conditional/MorleyHanfSchemaDischarge.lean) via the schema-completion construction — in fact without consuming the sequence's tail indiscernibility. Kept as a named Prop because the bridge theorems below are stated against it.

Equations

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

theorem FirstOrder.Language.morleySeedTailTemplateRealizable_of_tailTemplateRealizable {L' : Language} (h : TailTemplateRealizable) : MorleySeedTailTemplateRealizable

The broad (false-shaped) residual trivially implies the seed-restricted one — instantiation at s := morleySeed φ, dropping the extra source facts. Only the compact route uses this.

theorem FirstOrder.Language.tailTemplateRealizable_of_compact {L' : Language} (hCompact : ∀ (J : Type) [LinearOrder J] (S : Set (L'.withConstants J).Sentenceω), (∀ (F : Set (L'.withConstants J).Sentenceω), F.Finite → F ⊆ S → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model F N) → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model S N) : TailTemplateRealizable

The broad per-target compactness oracle implies the honest tail-template realizability residual: apply compactness to the (finitely-satisfiable) tail-template theory itself. Witnesses that TailTemplateRealizable is genuinely weaker than full compactness.

theorem FirstOrder.Language.hasArbLargeModels_of_seed_realizability {L' : Language} (hRealize : MorleySeedTailTemplateRealizable) (φ : L'.Sentenceω) (hφ : ∃ (M : Type) (x : L'.Structure M), φ.Realize M ∧ Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1)) : HasArbLargeModels φ

Morley–Hanf via seed-template realizability alone — no extraction (the definitive bridge). morleySeed_indiscernibleOn makes any extraction hypothesis unnecessary: an injective ℕ-sequence of the (infinite) source is already FULLY indiscernible on the Morley seed — the arity-0 members ignore their tuples and the disequality is absolute for injective sequences — so Infinite.natEmbedding supplies the sequence directly. No countable Ramsey, no Erdős–Rado. The EM template theory of the seed is realized via MorleySeedTailTemplateRealizable, and the model-form stretching of Methods/EM/TailAdapter.lean reads off φ-preservation and size.

theorem FirstOrder.Language.hasArbLargeModels_of_tail_realizability {L' : Language} (_hExtract : MorleyHanfExtractionTail) (hRealize : MorleySeedTailTemplateRealizable) (φ : L'.Sentenceω) (hφ : ∃ (M : Type) (x : L'.Structure M), φ.Realize M ∧ Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1)) : HasArbLargeModels φ

Morley–Hanf via tail extraction + seed-template realizability (historical form). The extraction hypothesis is SUBSUMED: morleySeed_indiscernibleOn shows an injective sequence is already fully indiscernible on the Morley seed, so the proof delegates to hasArbLargeModels_of_seed_realizability and does not consume hExtract. Kept as the historical statement shape from when the tail extraction was thought necessary.

theorem FirstOrder.Language.hasArbLargeModels_of_tail_extraction {L' : Language} (hExtract : MorleyHanfExtractionTail) (hCompact : ∀ (J : Type) [LinearOrder J] (S : Set (L'.withConstants J).Sentenceω), (∀ (F : Set (L'.withConstants J).Sentenceω), F.Finite → F ⊆ S → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model F N) → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model S N) (φ : L'.Sentenceω) (hφ : ∃ (M : Type) (x : L'.Structure M), φ.Realize M ∧ Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1)) : HasArbLargeModels φ

Legacy: Morley–Hanf via tail extraction + a broad compactness oracle. Kept for compatibility. The compactness oracle is stronger than needed: it asserts full L_{ω₁ω} compactness for every L'[[J]], which is false in general. It factors through the honest residual via tailTemplateRealizable_of_compact. Prefer hasArbLargeModels_of_tail_realizability.

Combinatorial residual via IsIndiscernibleOnSet

def FirstOrder.Language.IndiscernibleSequenceHypothesis {L' : Language} : Prop

Combinatorial residual (model-theoretic form): from a model of size ≥ ℶ_ω₁ under some chosen linear order on its carrier, produce an infinite strictly-monotone ℕ → M sequence whose range is IsIndiscernibleOnSet for the countable formula family s.

This is the Erdős–Rado content of MorleyHanfExtraction isolated from the model-theoretic plumbing: no reference to IsLomega1omegaIndiscernibleOn, no pairwise-distinct clause — only the combinatorial statement "large model + countable formula family ⇒ infinite homogeneous ω-sequence."

The hypothesis still quantifies over L, M, and formulas. The truly pure partition-calculus form is PureColoringHypothesis (below), which implies this via indiscernibleSequence_of_pureColoring.

FALSE-SHAPED (statement audit 2026-07-07). Sandwiched between two refutable statements: it is implied by PureColoringHypothesis (indiscernibleSequence_of_pureColoring) and implies the failed partition relation ℶ_ω₁ → (ω)^{<ω}_2 by interpreting colorings as relation symbols. See the Erdős-cardinal argument on PureColoringHypothesis below.

Equations

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

theorem FirstOrder.Language.morleyHanfExtraction_of_indiscernibleSequence {L' : Language} (hSeq : IndiscernibleSequenceHypothesis) : MorleyHanfExtraction

Reduction: the combinatorial residual IndiscernibleSequenceHypothesis implies MorleyHanfExtraction.

Given the hypothesis plus |M| ≥ ℶ_ω₁, equip M with a classical linear order (via WellOrderingRel / Classical.choice), apply the hypothesis to obtain a strict-monotone f : ℕ → M whose range is IsIndiscernibleOnSet for Set.range s. Strict-monotonicity gives pairwise distinctness (injectivity), and the sequence-level reduction IsIndiscernibleOnSet.toLomega1omegaIndiscernibleOn (Phase 2d0a) gives the restricted indiscernibility.

Pure partition-calculus residual

def FirstOrder.Language.PureColoringHypothesis : Prop

Pure partition-calculus residual: for every well-ordered type I with |I| ≥ ℶ_ω₁ and every countable family of Bool-valued colorings on finite-arity increasing tuples (order-embeddings) from I, there exists an infinite strictly-monotone ℕ → I sequence whose range is monochromatic for every coloring in the family.

The body mentions no language, no structure, no formula — only a well-ordered source (LinearOrder I + WellFoundedLT I), cardinalities, ℕ-indexed arities, and Bool colorings on Fin n ↪o I. This is the Erdős–Rado statement proper; Phase 2d targets it directly. indiscernibleSequence_of_pureColoring below proves that this implies the larger IndiscernibleSequenceHypothesis.

Note on the well-ordering assumption: arbitrary LinearOrder I does not admit strict-monotone ℕ → I in general (counterexample: I = ℕ with opposite order). The consumer chain always provides I as a canonical well-ordering of a model's carrier (via WellOrderingRel), so WellFoundedLT I is the right strengthening.

FALSE-SHAPED (statement audit 2026-07-07; external literature check, not formalized here). This statement is refutable in ZFC. One strictly monotone f : ℕ → I whose whole range is homogeneous for every coloring of every finite arity simultaneously is — already for one Bool coloring per arity — the partition relation ℶ_ω₁ → (ω)^{<ω}_2, which (the relation being upward closed in the source) holds iff the Erdős cardinal κ(ω), the least κ with κ → (ω)^{<ω}_2, satisfies κ(ω) ≤ ℶ_ω₁. But κ(ω) is inaccessible [Silver 1966/1970; Kanamori, The Higher Infinite, 2nd ed., §7, Props. 7.14(b), 7.15(b)]; an inaccessible κ has ℶ_α < κ for every α < κ (strong limit at successors, regularity at limits), and cf κ(ω) = κ(ω) > ω₁, so ℶ_ω₁ = sup_{α<ω₁} ℶ_α < κ(ω). Hence ℶ_ω₁ ↛ (ω)^{<ω}_2 is a theorem of ZFC, and no extraction can satisfy this hypothesis. The classical Morley/Hanf argument is consistent with this: it never produces one simultaneously-homogeneous set in the source — scheduled per-arity Erdős–Rado yields coherent finite approximations (an EM template certified through a consistency property), and the indiscernible sequence materializes only in the model built by Model Existence [Marker, Lectures on Infinitary Model Theory, §5.2]. The TRUE per-arity-bounded supply is finiteArityErdosRadoBounded (Combinatorics/FiniteArityErdosRadoInduction): one κ⁺-suborder homogeneous for all arities ≤ N, any finite N. Kept — like TailTemplateRealizable — as a strength marker and consumer interface; the bridges below remain true implications.

Equations

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

theorem FirstOrder.Language.indiscernibleSequence_of_pureColoring {L' : Language} (hPure : PureColoringHypothesis) : IndiscernibleSequenceHypothesis

Reduction: the pure partition-calculus hypothesis implies the model-theoretic IndiscernibleSequenceHypothesis. The colorings are instantiated as "truth of the i-th formula in s on the tuple's underlying function".

theorem FirstOrder.Language.pureColoringHypothesis_of_finiteArityErdosRadoOmega1 (h : FiniteArityErdosRadoOmega1 (Cardinal.beth 1)) : PureColoringHypothesis

Reduction: the finite-arity Erdős–Rado residual at color bound ℶ_1 implies the pure-coloring hypothesis. For each arity n, the countably many Bool colorings of that arity pack into ONE coloring with color type {i // (c i).1 = n} → Bool (size ≤ 2^{ℵ₀} = ℶ_1 — this is why the ER residual must take a color bound beyond ℵ₀); the single ω₁-homogeneous suborder restricts along its first ω elements (omegaOneNatEmb) to the required strictly-monotone ℕ-sequence, and per-coloring constancy is the packed constancy evaluated at the coloring's own index.

Compact-only Morley–Hanf headlines (LEGACY)

These wrappers collapse the proved reduction chain (hasArbLargeModels_of_restricted_extraction ∘ morleyHanfExtraction_of_indiscernibleSequence ∘ indiscernibleSequence_of_pureColoring) into a single theorem parameterized by the pure combinatorial hypothesis and a compactness oracle.

Legacy-shaped: the compactness oracle is no longer needed — the local EM route discharges the model-existence side, so morley_hanf_of_pureColoring (Methods/LocalEMOmegaResidual.lean) derives the Hanf bound from PureColoringHypothesis alone, and morley_hanf_of_finiteArityErdosRado from the ER-facing residual FiniteArityErdosRadoOmega1 ℶ_1 (via pureColoringHypothesis_of_finiteArityErdosRadoOmega1 above). Prefer those endpoints; the wrappers below are retained for compatibility.

theorem FirstOrder.Language.hasArbLargeModels_of_pureColoring_and_compact {L' : Language} [Countable ((l : ℕ) × L'.Relations l)] (hPure : PureColoringHypothesis) (hCompact : ∀ (J : Type) [LinearOrder J] (S : Set (L'.withConstants J).Sentenceω), (∀ (F : Set (L'.withConstants J).Sentenceω), F.Finite → F ⊆ S → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model F N) → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model S N) (φ : L'.Sentenceω) (hφ : ∃ (M : Type) (x : L'.Structure M), φ.Realize M ∧ Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1)) : HasArbLargeModels φ

Morley–Hanf reduction: assuming the pure combinatorial hypothesis PureColoringHypothesis and a per-target compactness oracle for every L'[[J]], any sentence satisfied in a model of size ≥ ℶ_ω₁ has arbitrarily large models.

Composes the proved chain: hPure → IndiscernibleSequenceHypothesis → MorleyHanfExtraction → HasArbLargeModels φ.

theorem FirstOrder.Language.morley_hanf_of_pureColoring_and_compact {L' : Language} [Countable ((l : ℕ) × L'.Relations l)] (hPure : PureColoringHypothesis) (hCompact : ∀ (J : Type) [LinearOrder J] (S : Set (L'.withConstants J).Sentenceω), (∀ (F : Set (L'.withConstants J).Sentenceω), F.Finite → F ⊆ S → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model F N) → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model S N) (φ : L'.Sentenceω) : IsHanfBound φ (Cardinal.beth (Ordinal.omega 1))

Morley–Hanf bound (compact + pure-coloring form): ℶ_ω₁ is a Hanf bound for every Lω₁ω sentence, assuming the pure partition-calculus hypothesis and a compactness oracle.

Specializes hasArbLargeModels_of_pureColoring_and_compact to the IsHanfBound shape used as the canonical Morley–Hanf endpoint.

Realizability-only Morley–Hanf via the proved tail extraction

The tail-weakened source extraction is now formalized (morleyHanfExtractionTail_holds, proved from infinite_ramsey_nat_family — countable Ramsey on ℕ, not an ℶ_{ω₁} Erdős–Rado schedule). Composing it with hasArbLargeModels_of_tail_realizability discharges the combinatorial hypothesis entirely: the theorems below take only the honest residual MorleySeedTailTemplateRealizable (realizability of the EM tail-template theory of the Morley seed {φ, x₀ ≠ x₁}, with the source facts).

That residual is itself now PROVED (morleySeedTailTemplateRealizable_holds, Conditional/MorleyHanfSchemaDischarge.lean — the schema-completion construction), so the unconditional endpoint morley_hanf there has no hypotheses at all. The hRealize-relative forms below remain the transparent intermediates; the *_compact wrappers are retained as legacy — their oracle is strictly stronger than needed.

theorem FirstOrder.Language.hasArbLargeModels_of_tail_realizable {L' : Language} (hRealize : MorleySeedTailTemplateRealizable) (φ : L'.Sentenceω) (hφ : ∃ (M : Type) (x : L'.Structure M), φ.Realize M ∧ Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1)) : HasArbLargeModels φ

Morley–Hanf reduction (realizability-only): assuming only the honest residual MorleySeedTailTemplateRealizable, any sentence satisfied in a model of size ≥ ℶ_ω₁ has arbitrarily large models. No combinatorial hypothesis at all — not even the (proved) tail extraction: an injective sequence is already seed-indiscernible (hasArbLargeModels_of_seed_realizability).

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

Morley–Hanf bound (realizability-only): ℶ_ω₁ is a Hanf bound for every Lω₁ω sentence, assuming only MorleySeedTailTemplateRealizable — which is itself proved (morleySeedTailTemplateRealizable_holds); see morley_hanf in Conditional/MorleyHanfSchemaDischarge.lean for the hypothesis-free endpoint. Consumes no extraction: the route is hasArbLargeModels_of_seed_realizability.

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

Historical alias of morley_hanf_of_seed_realizable (from when the route consumed the tail extraction).

theorem FirstOrder.Language.hasArbLargeModels_of_tail_compact {L' : Language} (hCompact : ∀ (J : Type) [LinearOrder J] (S : Set (L'.withConstants J).Sentenceω), (∀ (F : Set (L'.withConstants J).Sentenceω), F.Finite → F ⊆ S → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model F N) → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model S N) (φ : L'.Sentenceω) (hφ : ∃ (M : Type) (x : L'.Structure M), φ.Realize M ∧ Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1)) : HasArbLargeModels φ

Legacy (compact-only): Morley–Hanf reduction via a broad compactness oracle. Retained for compatibility; the per-target compactness oracle is strictly stronger than the honest residual TailTemplateRealizable (see tailTemplateRealizable_of_compact) and asserts full L_{ω₁ω} compactness, which is false in general. Prefer hasArbLargeModels_of_tail_realizable.

theorem FirstOrder.Language.morley_hanf_of_tail_compact {L' : Language} (hCompact : ∀ (J : Type) [LinearOrder J] (S : Set (L'.withConstants J).Sentenceω), (∀ (F : Set (L'.withConstants J).Sentenceω), F.Finite → F ⊆ S → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model F N) → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model S N) (φ : L'.Sentenceω) : IsHanfBound φ (Cardinal.beth (Ordinal.omega 1))

Legacy (compact-only): Morley–Hanf bound via a broad compactness oracle. Prefer morley_hanf_of_tail_realizable.

def FirstOrder.Language.HeightCex.Lang : Language

The counterexample language: unary predicates Pᵢ indexed by i : ℕ, nothing else.

Equations

• FirstOrder.Language.HeightCex.Lang = { Functions := fun (x : ℕ) => Empty, Relations := fun (n : ℕ) => match n with | 1 => ℕ | x => Empty }

instance FirstOrder.Language.HeightCex.instCountableRelationsLang (n : ℕ) : Countable (Lang.Relations n)

instance FirstOrder.Language.HeightCex.instCountableSigmaNatRelationsLang : Countable ((l : ℕ) × Lang.Relations l)

def FirstOrder.Language.HeightCex.Carrier : Type

The carrier: a set of size exactly ℶ_{ω₁}.

Equations

• FirstOrder.Language.HeightCex.Carrier = (Cardinal.beth (Ordinal.omega 1)).ord.ToType

theorem FirstOrder.Language.HeightCex.mk_Carrier : Cardinal.mk Carrier = Cardinal.beth (Ordinal.omega 1)

instance FirstOrder.Language.HeightCex.instInfiniteCarrier : Infinite Carrier

noncomputable def FirstOrder.Language.HeightCex.emb : ℕ ↪ Carrier

A copy of ℕ inside the carrier, along which heights are unbounded.

Equations

• FirstOrder.Language.HeightCex.emb = Infinite.natEmbedding FirstOrder.Language.HeightCex.Carrier

noncomputable def FirstOrder.Language.HeightCex.hgt (x : Carrier) : ℕ

The height of a carrier element: the inverse of emb on its range, arbitrary elsewhere.

Equations

• FirstOrder.Language.HeightCex.hgt x = Function.invFun (⇑FirstOrder.Language.HeightCex.emb) x

theorem FirstOrder.Language.HeightCex.hgt_emb (n : ℕ) : hgt (emb n) = n

@[implicit_reducible]

noncomputable instance FirstOrder.Language.HeightCex.instStructureLangCarrier : Lang.Structure Carrier

The height structure: Pᵢ x holds iff i ≤ hgt x.

Equations

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

def FirstOrder.Language.HeightCex.P (i : ℕ) : Lang.BoundedFormulaω Empty 1

The unary atom Pᵢ x₀.

Equations

• FirstOrder.Language.HeightCex.P i = FirstOrder.Language.BoundedFormulaω.rel (have this := i; this) fun (x : Fin 1) => FirstOrder.Language.var (Sum.inr 0)

def FirstOrder.Language.HeightCex.conj : Lang.BoundedFormulaω Empty 1

The countable conjunction ⋀ᵢ Pᵢ x₀.

Equations

• FirstOrder.Language.HeightCex.conj = FirstOrder.Language.BoundedFormulaω.iInf FirstOrder.Language.HeightCex.P

theorem FirstOrder.Language.HeightCex.realize_P (i : ℕ) (v : Empty → Carrier) (xs : Fin 1 → Carrier) : (P i).Realize v xs ↔ i ≤ hgt (xs 0)

def FirstOrder.Language.HeightCex.seed : ℕ → (n : ℕ) × Lang.BoundedFormulaω Empty n

The seed: ⋀ᵢ Pᵢ first, then every Pᵢ.

Equations

• FirstOrder.Language.HeightCex.seed 0 = ⟨1, FirstOrder.Language.HeightCex.conj⟩
• FirstOrder.Language.HeightCex.seed i.succ = ⟨1, FirstOrder.Language.HeightCex.P i⟩

noncomputable def FirstOrder.Language.HeightCex.a : ℕ → Carrier

The sequence of unboundedly growing height.

Equations

• FirstOrder.Language.HeightCex.a n = FirstOrder.Language.HeightCex.emb n

theorem FirstOrder.Language.HeightCex.strictMono_fin_one {β : Type u_1} [Preorder β] (w : Fin 1 → β) : StrictMono w

Every Fin 1-tuple is strictly monotone (vacuously).

theorem FirstOrder.Language.HeightCex.not_realize_conj (v : Empty → Carrier) (xs : Fin 1 → Carrier) : ¬conj.Realize v xs

⋀ᵢ Pᵢ fails at every carrier element (heights are finite).

theorem FirstOrder.Language.HeightCex.tail_indisc : IsLomega1omegaIndiscernibleOnTail a (Set.range seed)

a is tail-indiscernible on the seed: each Pᵢ (a n) is eventually true (cutoff i), and ⋀ᵢ Pᵢ (a n) is constantly false (cutoff 0).

theorem FirstOrder.Language.HeightCex.truth_P (i : ℕ) : (tailTemplateOfSeq a).truth (P i)

The tail template declares every Pᵢ true...

theorem FirstOrder.Language.HeightCex.not_truth_conj : ¬(tailTemplateOfSeq a).truth conj

... and ⋀ᵢ Pᵢ false.

theorem FirstOrder.Language.T_counterexample : ¬TailTemplateRealizable

The broad tail-template residual is refutable (the height-model counterexample of the TailTemplateRealizable docstring, formalized): over the language of unary predicates Pᵢ, the height model of size ℶ_{ω₁} with the seed {⋀ᵢ Pᵢ} ∪ {Pᵢ}ᵢ and the sequence a n of height n is tail-indiscernible on the seed, but its tail-template theory contains every positive Pᵢ(c₀) together with ¬⋀ᵢ Pᵢ(c₀) — unsatisfiable. So the ∀-sequence residual is a genuine L_{ω₁ω} compactness failure; only the Morley-seed form (MorleySeedTailTemplateRealizable) can be the honest target.