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

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).

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.

source

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.

Instances For

Combinatorial residual via `IsIndiscernibleOnSet` #

Pure partition-calculus residual #

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.

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.

source

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.

source

def FirstOrder.Language.HeightCex.Lang :

Language

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

Equations