EM Realization: Admissible/Barwise Adapter Layer

This file contains the theorems that connect the EM template-theory machinery (from Realization.lean) to the admissible-fragment infrastructure. These are the _of_fragment, _of_fullFragment, and _of_compact endpoints that take FiniteCompactFragment, FullBarwiseFragment, or bare compactness hypotheses.

Separated from Realization.lean so that the Countable import bundle can import the core EM machinery without transitively pulling in admissible-fragment infrastructure. The adapter layer lives in the Admissible bundle instead.

Model of templateTheoryOn via Barwise compactness

theorem FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOn_model_of_fragment {L : Language} (T : L.Lomega1omegaTemplate) (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) {J : Type u} [LinearOrder J] (A : (L.withConstants J).FiniteCompactFragment) (hSub : T.templateTheoryOn Γ J ⊆ A.formulas) (hfin : ∀ (F : Set (L.withConstants J).Sentenceω), F.Finite → F ⊆ T.templateTheoryOn Γ J → ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model F N) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model (T.templateTheoryOn Γ J) N

Abstract Barwise wrapper for the restricted template theory.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.templateTheoryOn_model_of_fragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {J : Type u} [LinearOrder J] (Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)) (A : (L.withConstants J).FiniteCompactFragment) (hSub : h.template.templateTheoryOn Γ J ⊆ A.formulas) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model (h.template.templateTheoryOn Γ J) N

Indiscernible specialization of templateTheoryOn_model_of_fragment.

Sequence-indexed adapter wrappers

theorem FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOfSeq_model_of_fragment {L : Language} {J : Type u} [LinearOrder J] (T : L.Lomega1omegaTemplate) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (A : (L.withConstants J).FiniteCompactFragment) (hSub : T.templateTheoryOfSeq s J ⊆ A.formulas) (hfin : ∀ (F : Set (L.withConstants J).Sentenceω), F.Finite → F ⊆ T.templateTheoryOfSeq s J → ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model F N) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model (T.templateTheoryOfSeq s J) N

Abstract Barwise wrapper for templateTheoryOfSeq.

theorem FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOfSeq_model_of_fullFragment {L : Language} {J : Type u} [LinearOrder J] (T : L.Lomega1omegaTemplate) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (B : (L.withConstants J).FullBarwiseFragment) (hfin : ∀ (F : Set (L.withConstants J).Sentenceω), F.Finite → F ⊆ T.templateTheoryOfSeq s J → ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model F N) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model (T.templateTheoryOfSeq s J) N

Full-Barwise-fragment specialization.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.templateTheoryOfSeq_model_of_fragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {J : Type u} [LinearOrder J] (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (A : (L.withConstants J).FiniteCompactFragment) (hSub : h.template.templateTheoryOfSeq s J ⊆ A.formulas) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model (h.template.templateTheoryOfSeq s J) N

Sequence-indexed model_of_fragment for indiscernible source.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.templateTheoryOfSeq_model_of_fullFragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {J : Type u} [LinearOrder J] (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (B : (L.withConstants J).FullBarwiseFragment) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model (h.template.templateTheoryOfSeq s J) N

Caller-ready EM-realization from a full Barwise fragment.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.templateTheoryOfSeq_model_of_fullFragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOn a (Set.range s)) {J : Type u} [LinearOrder J] (B : (L.withConstants J).FullBarwiseFragment) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model ((templateOfSeq a).templateTheoryOfSeq s J) N

Caller-ready EM-realization from a full Barwise fragment, under restricted indiscernibility.

Stretching along an arbitrary target order

These theorems package the existing templateTheoryOfSeq pipeline into caller-ready form: from an indiscernible template they produce a target L[[J]]-structure N whose constants satisfy the template on formulas in Set.range s (the countable family named by the enumeration s). The target order J is an arbitrary linear order — including uncountable target orders, which is where Morley–Hanf cardinality amplification lives.

Two forms are provided:

• stretch_restricted_of_fullFragment / _of_compact use Sentenceω.Realize (templateSentence φ t) N as the conclusion — this is the form the template theory literally delivers.
• stretch_restricted_sequence_of_fullFragment / _of_compact produce an explicit b : J → N sequence and conclude φ.Realize Empty.elim (b ∘ t) ↔ h.template.truth φ, via the bridge realize_templateSentence_of_structure.

Scope: these theorems do NOT claim full IsLomega1omegaIndiscernible for any extracted sequence — that would require enumerating all Lω₁ω formulas, which is not currently formalized. They DO allow uncountable J, which is what cardinality amplification for MorleyHanfTransfer eventually needs; the residual step is extracting an indiscernible source sequence of length I ≥ ℶ_ω₁ from a large model (the Erdős–Rado half, not addressed here).

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.stretch_restricted_of_fullFragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) {J : Type u} [LinearOrder J] (B : (L.withConstants J).FullBarwiseFragment) : ∃ (N : Type) (x : (L.withConstants J).Structure N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (Lomega1omegaTemplate.templateSentence (s i).snd t).Realize N ↔ h.template.truth (s i).snd

EM stretching along an arbitrary target order (full Barwise fragment).

Given an Lω₁ω-indiscernible sequence a : I → M over an infinite linear order I, a formula enumeration s : ℕ → Σ n, L.BoundedFormulaω Empty n, and a linear order J with a full Barwise fragment for L[[J]], there exists a target L[[J]]-structure N such that for every index i : ℕ and every strictly-increasing tuple t : Fin (s i).1 ↪o J, the realization of templateSentence (s i).2 t in N matches the truth value of (s i).2 in the source template.

The conclusion is quantified over i : ℕ (equivalently, over formulas in Set.range s) — this is restricted indiscernibility. Full Lω₁ω-indiscernibility of the J-indexed constants would additionally require a countable enumeration of all Lω₁ω formulas.

theorem FirstOrder.Language.realize_templateSentence_of_structure {L : Language} {J : Type u} [LinearOrder J] {N : Type u_1} [(L.withConstants J).Structure N] {n : ℕ} (φ : L.BoundedFormulaω Empty n) (t : Fin n ↪o J) : (Lomega1omegaTemplate.templateSentence φ t).Realize N ↔ φ.Realize Empty.elim fun (i : Fin n) => Term.realize Empty.elim (func (Sum.inr (t i)) Fin.elim0)

Generalized realize_templateSentence.

Like realize_templateSentence (InfinitaryLogic/Methods/EM/Realization.lean:97), but takes an arbitrary [L[[J]].Structure N] instead of requiring the L[[J]]-structure to be built from a specific σ : J → M via constantsOn.structure σ. The L-structure on N is derived from the L[[J]]-structure via the canonical reduct along lhomWithConstants L J.

The right-hand side realizes φ on the sequence fun i => b (t i), where b j is the closed-term realization of the constant symbol Sum.inr j (i.e., the interpretation of the J-indexed constant in the given L[[J]]-structure on N).

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.stretch_restricted_sequence_of_fullFragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) {J : Type u} [LinearOrder J] (B : (L.withConstants J).FullBarwiseFragment) : ∃ (N : Type) (x : (L.withConstants J).Structure N) (b : J → N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (s i).snd.Realize Empty.elim (b ∘ ⇑t) ↔ h.template.truth (s i).snd

EM stretching along an arbitrary target order — sequence form (full Barwise fragment).

Corollary of stretch_restricted_of_fullFragment via the bridge realize_templateSentence_of_structure: produces an explicit b : J → N sequence such that for every i : ℕ and every strictly-increasing tuple t : Fin (s i).1 ↪o J, the realization of (s i).2 on b ∘ t matches h.template.truth (s i).2.

The sequence b is defined as the interpretation of the J-indexed constant symbol under the L[[J]]-structure. The L-structure used for .Realize is the reduct along lhomWithConstants L J, introduced via letI inside the existential body.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.templateTheoryOfSeq_model_of_compact {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) {J : Type u} [LinearOrder J] (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (height : Ordinal.{0}) (h_height : Ordinal.omega0 < height) (hCompact : ∀ (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) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model (h.template.templateTheoryOfSeq s J) N

EM realization from a bare compactness hypothesis.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.stretch_restricted_of_compact {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) {J : Type u} [LinearOrder J] (height : Ordinal.{0}) (h_height : Ordinal.omega0 < height) (hCompact : ∀ (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) : ∃ (N : Type) (x : (L.withConstants J).Structure N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (Lomega1omegaTemplate.templateSentence (s i).snd t).Realize N ↔ h.template.truth (s i).snd

EM stretching along an arbitrary target order (bare compactness oracle).

Same content as stretch_restricted_of_fullFragment, but driven by a bare compactness hypothesis on L[[J]] instead of a FullBarwiseFragment.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.stretch_restricted_sequence_of_compact {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) {J : Type u} [LinearOrder J] (height : Ordinal.{0}) (h_height : Ordinal.omega0 < height) (hCompact : ∀ (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) : ∃ (N : Type) (x : (L.withConstants J).Structure N) (b : J → N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (s i).snd.Realize Empty.elim (b ∘ ⇑t) ↔ h.template.truth (s i).snd

EM stretching along an arbitrary target order — sequence form (bare compactness oracle).

Compact-oracle variant of stretch_restricted_sequence_of_fullFragment.

Morley–Hanf-oriented corollaries

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.stretch_preserves_sentence_of_fullFragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (φ : L.BoundedFormulaω Empty 0) (hφ : ⟨0, φ⟩ ∈ Set.range s) {J : Type u} [LinearOrder J] (B : (L.withConstants J).FullBarwiseFragment) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Sentenceω.Realize φ N ↔ Sentenceω.Realize φ M

Sentence preservation under EM stretching.

If the formula family s enumerates a sentence φ : L.BoundedFormulaω Empty 0 (i.e., ⟨0, φ⟩ ∈ Set.range s), then the stretched model N realizes φ iff the source model M does.

This is the form Morley–Hanf needs: any sentence M satisfies survives to the stretched model.

def FirstOrder.Language.disEqFormula {L : Language} : L.BoundedFormulaω Empty 2

The 2-ary Lω₁ω disequality formula x₀ ≠ x₁.

Equations

• FirstOrder.Language.disEqFormula = (FirstOrder.Language.BoundedFormulaω.equal (FirstOrder.Language.var (Sum.inr 0)) (FirstOrder.Language.var (Sum.inr 1))).not

def FirstOrder.Language.morleySeed {L : Language} (φ : L.Sentenceω) : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n

The Morley seed of a sentence φ: the concrete two-formula family the Morley–Hanf tail bridge feeds the EM machinery — φ itself, the disequality x₀ ≠ x₁, and repeated φ-filler. The honest tail-template residual quantifies over exactly this seed (MorleySeedTailTemplateRealizable in Conditional/MorleyHanfTransfer.lean), NOT over arbitrary formula sequences: an arbitrary sequence can enumerate {Pᵢ x}ᵢ ∪ {⋀ᵢ Pᵢ x} against a "height" model, whose tail template is finitely satisfiable but unsatisfiable — a genuine L_{ω₁ω} compactness failure.

Equations

• FirstOrder.Language.morleySeed φ 0 = ⟨0, φ⟩
• FirstOrder.Language.morleySeed φ 1 = ⟨2, FirstOrder.Language.disEqFormula⟩
• FirstOrder.Language.morleySeed φ n.succ.succ = ⟨0, φ⟩

@[simp]

theorem FirstOrder.Language.morleySeed_zero {L : Language} (φ : L.Sentenceω) : morleySeed φ 0 = ⟨0, φ⟩

@[simp]

theorem FirstOrder.Language.morleySeed_one {L : Language} (φ : L.Sentenceω) : morleySeed φ 1 = ⟨2, disEqFormula⟩

theorem FirstOrder.Language.morleySeed_indiscernibleOn {L : Language} {M : Type u_1} [L.Structure M] (φ : L.Sentenceω) {a : ℕ → M} (ha : ∀ (i j : ℕ), i ≠ j → a i ≠ a j) : IsLomega1omegaIndiscernibleOn a (Set.range (morleySeed φ))

The Morley seed needs no extraction: ANY pairwise-distinct sequence is fully Lω₁ω-indiscernible on Set.range (morleySeed φ) — the arity-0 members ignore their tuples, and the disequality is true on every strictly monotone pair of a pairwise-distinct sequence. This is why the definitive Morley–Hanf route consumes no Ramsey/Erdős–Rado extraction at all: Infinite.natEmbedding already supplies a seed-indiscernible sequence.

theorem FirstOrder.Language.IsLomega1omegaIndiscernible.stretch_injective_of_fullFragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (h : IsLomega1omegaIndiscernible a) (hPairwise : ∀ {i j : I}, i ≠ j → a i ≠ a j) (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (hDisEq : ⟨2, disEqFormula⟩ ∈ Set.range s) {J : Type u} [LinearOrder J] (B : (L.withConstants J).FullBarwiseFragment) : ∃ (N : Type) (x : (L.withConstants J).Structure N) (b : J → N), Function.Injective b

Injectivity of the stretched sequence.

If the source sequence a : I → M is pairwise distinct on its index set and the formula family s enumerates the 2-ary disequality formula (disEqFormula : L.BoundedFormulaω Empty 2), then the stretched sequence b : J → N is injective. Hence #N ≥ #J: cardinality is amplified from I to J.

Restricted-indiscernibility variants

These _on theorems take IsLomega1omegaIndiscernibleOn a (Set.range s) instead of the full IsLomega1omegaIndiscernible a, and state their conclusions against (templateOfSeq a).truth rather than h.template.truth. Tranche 2b of the Phase 2 refactor.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.templateTheoryOfSeq_model_of_compact {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOn a (Set.range s)) {J : Type u} [LinearOrder J] (height : Ordinal.{0}) (h_height : Ordinal.omega0 < height) (hCompact : ∀ (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) : ∃ (N : Type) (x : (L.withConstants J).Structure N), Theoryω.Model ((templateOfSeq a).templateTheoryOfSeq s J) N

Compact-oracle adapter under restricted indiscernibility.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.stretch_restricted_of_fullFragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOn a (Set.range s)) {J : Type u} [LinearOrder J] (B : (L.withConstants J).FullBarwiseFragment) : ∃ (N : Type) (x : (L.withConstants J).Structure N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (Lomega1omegaTemplate.templateSentence (s i).snd t).Realize N ↔ (templateOfSeq a).truth (s i).snd

EM stretching (sentence form, fullFragment, restricted source).

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.stretch_restricted_of_compact {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOn a (Set.range s)) {J : Type u} [LinearOrder J] (height : Ordinal.{0}) (h_height : Ordinal.omega0 < height) (hCompact : ∀ (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) : ∃ (N : Type) (x : (L.withConstants J).Structure N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (Lomega1omegaTemplate.templateSentence (s i).snd t).Realize N ↔ (templateOfSeq a).truth (s i).snd

EM stretching (sentence form, compact oracle, restricted source).

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.stretch_restricted_sequence_of_fullFragment {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOn a (Set.range s)) {J : Type u} [LinearOrder J] (B : (L.withConstants J).FullBarwiseFragment) : ∃ (N : Type) (x : (L.withConstants J).Structure N) (b : J → N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (s i).snd.Realize Empty.elim (b ∘ ⇑t) ↔ (templateOfSeq a).truth (s i).snd

EM stretching (sequence form, fullFragment, restricted source).

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOn.stretch_restricted_sequence_of_compact {L : Language} {I : Type w} [LinearOrder I] [Infinite I] {M : Type} [L.Structure M] {a : I → M} (s : ℕ → (n : ℕ) × L.BoundedFormulaω Empty n) (h : IsLomega1omegaIndiscernibleOn a (Set.range s)) {J : Type u} [LinearOrder J] (height : Ordinal.{0}) (h_height : Ordinal.omega0 < height) (hCompact : ∀ (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) : ∃ (N : Type) (x : (L.withConstants J).Structure N) (b : J → N), ∀ (i : ℕ) (t : Fin (s i).fst ↪o J), (s i).snd.Realize Empty.elim (b ∘ ⇑t) ↔ (templateOfSeq a).truth (s i).snd

EM stretching (sequence form, compact oracle, restricted source).