The local EM template-realization bridge

The adapter between the local EM truth-lemma stack (LocalEMTruthLemma.lean) and the honest Morley–Hanf residual MorleySeedTailTemplateRealizable (Conditional/MorleyHanfTransfer.lean), parameterized by the restricted OmegaCompleteForColim (the exact ΓlocalColim-restricted completeness the truth lemma consumes — not the strictly stronger global OmegaComplete). Four deliverables:

1. LocalStage.ofSeq — the seed stage of a formula sequence s : ℕ → Σ n, L'.BoundedFormulaω Empty n, with Γ₀ = Set.range s. Note the countability interface: LocalStage requires countably many function and relation symbols, while TailTemplateRealizable assumes only countable relations — the function-symbol countability is an explicit extra instance argument of this bridge for now (a later chunk can pass to the countable sublanguage generated by s).

2. Subsequence-preserving extraction (exists_orderEmb_tailIndiscernible_ΓEMlocal): from the given sequence a : ℕ → M, an order embedding g : ℕ ↪o ℕ with a ∘ g tail-indiscernible on ΓEMlocal s₀. No fresh Infinite.natEmbedding M (contrast exists_ΓEMlocal_tail_indiscernible, which extracts an unrelated sequence and so loses the input's template): the Ramsey colorings of infinite_ramsey_nat_family are pulled back along the input a, so no cardinality hypothesis on M is consumed. exists_localEMContext_subseq packages the result as a LocalEMContext with ctx.a = a ∘ g and ctx.Γ = ΓEMlocal s₀.

3. Template preservation under subsequence (IsLomega1omegaIndiscernibleOnTail.tailTemplateOfSeq_comp_truth_iff): for ⟨n, φ⟩ ∈ Γ and a tail-indiscernible on Γ, the eventually-form template of a ∘ g agrees with that of a. The key adapter preventing the wrong template: the final residual is about the template of the input sequence a, while the truth lemma runs over the extracted ctx.a = a ∘ g. templateTheoryOn_congr transports the template theory across the agreement.

4. The parameterized EM model theorem: realize_templateSentence_localEM_iff — in the local EM term model, a template sentence over the seed language holds iff the eventually-form template of ctx.a declares its formula true (via deFormClosedForColim_of_ΓEMlocal_subset, TLReadyStage_of_Γlocal, truthLemmaStage_of_mem, and realize_templateSentence_of_structure) — and its packaging LocalEMContext.templateTheoryOn_seed_model: the quotient model satisfies every positive/negative sentence of the seed-family template theory.

Acceptance (tailTemplateRealizable_of_localEM): given a tail-indiscernible-on-Set.range s input a and, for that s, an extracted subsequence context that is OmegaCompleteForColim, the tail-template theory of a over any target order J has a model. This per-s lemma is hypothesis-relative and true as stated — but its ∀-s closure is false-shaped (a seed enumerating {Pᵢ x}ᵢ ∪ {⋀ᵢ Pᵢ x} against a height model has a finitely-satisfiable, unsatisfiable tail-template theory; see TailTemplateRealizable's docstring in Conditional/MorleyHanfTransfer.lean), so no named residual quantifies over arbitrary s. The named residuals are seed-specific and source-aware: MorleySeedOmegaExtraction (the acceptance bundle at s := morleySeed φ, carrying Sentenceω.Realize φ M, the ℶ_{ω₁} size premise, and pairwise distinctness) and its cleanest form MorleySeedOmegaHomogeneousExtraction — the J-free source-side homogeneity residual (via omegaCompleteForColim_of_omegaHomogeneous and morleySeedOmegaExtraction_of_homogeneousExtraction): a countable-family homogeneity extraction statement about a ∘ g on the seed family — no term model, no quotients, no supports.

This file imports the EM-side template machinery (Methods/EM/TailAdapter.lean), so it is NOT part of the pure local stack guarded by check_local_boundary.sh's EM-free roots; it must stay Conditional-free (checked by the same script), leaving TailTemplateRealizable itself to a downstream Conditional-touching file.

1. The seed stage of a formula sequence

@[reducible]

def FirstOrder.Language.LocalStage.ofSeq (L' : Language) [hf : Countable ((n : ℕ) × L'.Functions n)] [hr : Countable ((n : ℕ) × L'.Relations n)] (s : ℕ → (n : ℕ) × L'.BoundedFormulaω Empty n) : LocalStage

The seed stage of a formula sequence: stage language L', stage family Set.range s. The countability certificates are instance arguments; note TailTemplateRealizable itself assumes only countably many relation symbols, so the function-symbol countability is an extra assumption of this bridge for now (a later chunk can replace L' by the countable sublanguage generated by s).

Equations

• FirstOrder.Language.LocalStage.ofSeq L' s = { Lang := L', Gamma := Set.range s, gamma_countable := ⋯, fun_countable := hf, rel_countable := hr }

@[simp]

theorem FirstOrder.Language.LocalStage.ofSeq_Lang (L' : Language) [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] (s : ℕ → (n : ℕ) × L'.BoundedFormulaω Empty n) : (ofSeq L' s).Lang = L'

@[simp]

theorem FirstOrder.Language.Γlocal_ofSeq_zero (L' : Language) [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] (s : ℕ → (n : ℕ) × L'.BoundedFormulaω Empty n) : Γlocal (LocalStage.ofSeq L' s) 0 = Set.range s

Skeleton-constant terms: support and deep interpretation

theorem FirstOrder.Language.locJSupport_constTerm (Λ : Language) (J : Type) [LinearOrder J] (j : J) : Λ.locJSupport J (func (Sum.inr j) Fin.elim0) = {j}

The skeleton support of a skeleton-constant term is the singleton of its index.

theorem FirstOrder.Language.locDeepInterp_constTerm (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (d : ℕ) (S : Finset J) (j : J) : Λ.locDeepInterp J a d S (func (Sum.inr j) Fin.elim0) = a (d + deepRank J S j)

The deep interpretation of a skeleton-constant term is the deep sequence at the constant's rank position — the semantic content of "the J-skeleton is interpreted by the deep tuple". Definitional: the sum/constantsOn funMap coherence reduces.

2. Subsequence-preserving extraction

The Ramsey colorings are pulled back along the input sequence a, so the extracted tail-indiscernible sequence is a subsequence a ∘ g (preserving a's template, per §3) and no cardinality hypothesis on M is consumed — contrast exists_ΓEMlocal_tail_indiscernible, whose Infinite.natEmbedding discards the input sequence.

theorem FirstOrder.Language.exists_orderEmb_tailIndiscernible_ΓEMlocal (s₀ : LocalStage) (M : Type) [s₀.Lang.Structure M] [Nonempty M] (a : ℕ → M) : ∃ (g : ℕ ↪o ℕ), IsLomega1omegaIndiscernibleOnTail (a ∘ ⇑g) (ΓEMlocal s₀)

Subsequence-preserving extraction: some subsequence of the given a is tail-indiscernible on the whole countable local family ΓEMlocal s₀. Infinite-Ramsey on the formula-truth colorings of increasing a-tuples, via infinite_ramsey_nat_family.

theorem FirstOrder.Language.exists_localEMContext_subseq (s₀ : LocalStage) (J : Type) [LinearOrder J] (M : Type) [s₀.Lang.Structure M] [Nonempty M] (a : ℕ → M) : ∃ (g : ℕ ↪o ℕ) (ctx : (localColim s₀).LocalEMContext J), ctx.a = a ∘ ⇑g ∧ ctx.Γ = ΓEMlocal s₀

The subsequence context: the extraction packaged as an actual LocalEMContext with ctx.a = a ∘ g and ctx.Γ = ΓEMlocal s₀ (membership obligations from the ΓEMlocal dischargers). This proves every conjunct of the acceptance theorem's hOmega bundle except ctx.OmegaCompleteForColim — the one honest hole this file leaves open.

3. Template preservation under subsequence

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.tailTemplateOfSeq_comp_truth_iff {L : Language} {M : Type u_1} [L.Structure M] {a : ℕ → M} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (h : IsLomega1omegaIndiscernibleOnTail a Γ) (g : ℕ ↪o ℕ) {n : ℕ} {φ : L.BoundedFormulaω Empty n} (hφ : ⟨n, φ⟩ ∈ Γ) : (tailTemplateOfSeq (a ∘ ⇑g)).truth φ ↔ (tailTemplateOfSeq a).truth φ

Template preservation under subsequence (the key adapter preventing the wrong template): for a family formula, the eventually-form template of a subsequence a ∘ g agrees with that of a, provided a is tail-indiscernible on the family. Both directions route through a's truth collapse (tailTemplateOfSeq_truth_iff), using that g-images of deep tuples are deep (StrictMono.le_apply).

theorem FirstOrder.Language.Lomega1omegaTemplate.templateTheoryOn_congr {L : Language} {T T' : L.Lomega1omegaTemplate} {Γ : Set ((n : ℕ) × L.BoundedFormulaω Empty n)} (h : ∀ (n : ℕ) (φ : L.BoundedFormulaω Empty n), ⟨n, φ⟩ ∈ Γ → (T.truth φ ↔ T'.truth φ)) (J : Type u) [LinearOrder J] : T.templateTheoryOn Γ J = T'.templateTheoryOn Γ J

Templates that agree on a family generate the same restricted template theory. Transports templateTheoryOn (hence templateTheoryOfSeq) across the subsequence agreement of the previous lemma.

4. The parameterized EM model theorem

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.seedOfΓEMlocal (s₀ : LocalStage) {M : Type} [s₀.Lang.Structure M] [Nonempty M] {a' : ℕ → M} {Γ : Set ((n : ℕ) × (localColim s₀).BoundedFormulaω Empty n)} (hΓ : ΓEMlocal s₀ ⊆ Γ) (h : IsLomega1omegaIndiscernibleOnTail a' Γ) : IsLomega1omegaIndiscernibleOnTail a' (Γlocal s₀ 0)

Seed restriction of tail indiscernibility: a sequence tail-indiscernible (over the colimit structure) on a family containing ΓEMlocal s₀ is tail-indiscernible, over the seed language, on the seed family Γlocal s₀ 0 — via the colimit membership of seed images and the semantic transport realize_map_LlocalInclusion.

theorem FirstOrder.Language.IsLomega1omegaIndiscernibleOnTail.seedOfΓEMlocal_of_reduct (s₀ : LocalStage) {M : Type} [(localColim s₀).Structure M] {a' : ℕ → M} {Γ : Set ((n : ℕ) × (localColim s₀).BoundedFormulaω Empty n)} (hΓ : ΓEMlocal s₀ ⊆ Γ) (h : IsLomega1omegaIndiscernibleOnTail a' Γ) : IsLomega1omegaIndiscernibleOnTail a' (Γlocal s₀ 0)

Seed restriction of tail indiscernibility, generic core: over ANY localColim structure, the seed-language reduct transports tail indiscernibility on a family containing ΓEMlocal s₀ down to the seed family — the second canonical-structure dependency of the realization chain, generalized. For the canonical structure this reduct is definitionally the original seed structure.

theorem FirstOrder.Language.realize_templateSentence_localEM_iff_of_skolemUniversal (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (hsk : LocalSkolemUniversalForColim s₀) (ctx : (localColim s₀).LocalEMContext J) : ΓEMlocal s₀ ⊆ ctx.Γ → LocalEMContext.OmegaCompleteForColim s₀ J ctx → ∀ {n : ℕ} (φ : s₀.Lang.BoundedFormulaω Empty n), ⟨n, φ⟩ ∈ Γlocal s₀ 0 → ∀ (t : Fin n ↪o J), (Lomega1omegaTemplate.templateSentence φ t).Realize (LocalEMContext.Carrier (localColim s₀) J ctx) ↔ (tailTemplateOfSeq ctx.a).truth φ

The key realization equivalence, generic core: over ANY localColim source structure satisfying the Skolem-universality mixin, with the source's seed semantics read through the seed-language reduct. Same chain as the canonical version below, fed by the generic staged truth lemma and the generic seed restriction.

theorem FirstOrder.Language.LocalEMContext.templateTheoryOn_seed_model_of_skolemUniversal (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (hsk : LocalSkolemUniversalForColim s₀) (ctx : (localColim s₀).LocalEMContext J) : ΓEMlocal s₀ ⊆ ctx.Γ → OmegaCompleteForColim s₀ J ctx → Theoryω.Model ((tailTemplateOfSeq ctx.a).templateTheoryOn (Γlocal s₀ 0) J) (Carrier (localColim s₀) J ctx)

The parameterized EM model theorem, generic core: the quotient model satisfies the seed template theory of ctx.a, over any mixin-satisfying source with seed semantics through the reduct.

theorem FirstOrder.Language.realize_templateSentence_localEM_iff (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [s₀.Lang.Structure M] [Nonempty M] (ctx : (localColim s₀).LocalEMContext J) : ΓEMlocal s₀ ⊆ ctx.Γ → LocalEMContext.OmegaCompleteForColim s₀ J ctx → ∀ {n : ℕ} (φ : s₀.Lang.BoundedFormulaω Empty n), ⟨n, φ⟩ ∈ Γlocal s₀ 0 → ∀ (t : Fin n ↪o J), (Lomega1omegaTemplate.templateSentence φ t).Realize (LocalEMContext.Carrier (localColim s₀) J ctx) ↔ (tailTemplateOfSeq ctx.a).truth φ

The key realization equivalence: in the local EM term model (over any context with ΓEMlocal-closure and OmegaComplete), a template sentence over the seed language holds iff the eventually-form template of ctx.a declares its formula true. The chain: constant terms realize as their term classes (constMap_mkClass); the language maps peel off (realize_templateSentence_of_structure + realize_mapLanguage twice); the staged truth lemma (truthLemmaStage_of_mem, fed by TLReadyStage_of_Γlocal and the discharged deForm mixin) converts to eventual deep truth; the deep interpretation of the J-skeleton is a deep tuple of ctx.a (locDeepInterp_constTerm), so the truth collapse of tail indiscernibility finishes.

theorem FirstOrder.Language.LocalEMContext.templateTheoryOn_seed_model (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [s₀.Lang.Structure M] [Nonempty M] (ctx : (localColim s₀).LocalEMContext J) : ΓEMlocal s₀ ⊆ ctx.Γ → OmegaCompleteForColim s₀ J ctx → Theoryω.Model ((tailTemplateOfSeq ctx.a).templateTheoryOn (Γlocal s₀ 0) J) (Carrier (localColim s₀) J ctx)

The parameterized EM model theorem: the local EM quotient model satisfies every positive/negative sentence of the seed-family template theory of ctx.a — for any context with ΓEMlocal-closure, assuming OmegaComplete. Positive sentences by the key equivalence; negative ones by its contrapositive.

Full indiscernibility restores Ω-completeness

The refuted Ω-residuals all fail on drift: a tail-indiscernible sequence lets the truth value of a de-substituted component at the depth-d consecutive tuple vary with d below its cutoff, so the witnessing component of a countable connective can escape to infinity. Under full (cutoff-0) restricted indiscernibility — IsLomega1omegaIndiscernibleOn, the classical Erdős–Rado extraction output, whose production genuinely consumes the ℶ_{ω₁} premise (e.g. in the height model it must move off the growing diagonal into a single large height fiber) — every de-substituted formula in the family has ONE value on all strictly monotone tuples, so witnesses cannot drift and the Ω-clauses hold outright.

theorem FirstOrder.Language.LocalEMContext.omegaCompleteOn_of_indiscernibleOn {Λ : Language} (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (hfull : IsLomega1omegaIndiscernibleOn ctx.a ctx.Γ) {Γ' : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)} (hSup : ∀ {m : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty m), ⟨m, BoundedFormulaω.iSup φs⟩ ∈ Γ' → ∀ (i : ℕ) (ts : Fin m → (Λ.withConstants J).Term Empty) (S : Finset J) (hcov : ∀ (i : Fin m), Λ.locJSupport J (ts i) ⊆ S), ⟨S.card, Λ.locDeForm J S (φs i) ts hcov⟩ ∈ ctx.Γ) (hInf : ∀ {m : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty m), ⟨m, BoundedFormulaω.iInf φs⟩ ∈ Γ' → ∀ (i : ℕ) (ts : Fin m → (Λ.withConstants J).Term Empty) (S : Finset J) (hcov : ∀ (i : Fin m), Λ.locJSupport J (ts i) ⊆ S), ⟨S.card, Λ.locDeForm J S (φs i) ts hcov⟩ ∈ ctx.Γ) : OmegaCompleteOn Λ J ctx Γ'

Full indiscernibility restores the (refuted-for-tail) Ω-completeness: if the context's sequence is fully indiscernible on its family and the family contains the de-substituted components of the Γ' disjunctions/conjunctions, then the support-covered Ω-clauses hold — each component's eventual deep truth is a d-independent value, so a witness at one depth is a witness at every depth. This is the reduction that replaces the false tail-side residuals; its intended supply was the classical full-indiscernibility extraction (MorleyHanfExtraction-shaped), not any atTop cutoff exchange — but that extraction was itself found false-shaped (statement audit 2026-07-07; see its docstring), so the supply must come from a fully indiscernible sequence in a constructed model (the template / consistency-property route), where this reduction applies unchanged.

theorem FirstOrder.Language.LocalEMContext.omegaCompleteForColim_of_indiscernibleOn (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (ctx : (localColim s₀).LocalEMContext J) (hΓ : ΓEMlocal s₀ ⊆ ctx.Γ) (hfull : IsLomega1omegaIndiscernibleOn ctx.a ctx.Γ) : OmegaCompleteForColim s₀ J ctx

The colimit-family Ω-completeness from full indiscernibility, discharged: for a context whose family contains ΓEMlocal and whose sequence is fully indiscernible on it, the support-covered OmegaCompleteForColim holds outright — the component memberships come from the constructor-inversion plumbing (iSup/iInf_component_mem_ΓlocalColim) composed with the deForm discharger (locDeForm_mem_ΓEMlocal). This replaces the (refuted) tail-side residuals as the route into the truth lemma: what remains is producing the fully indiscernible sequence. The in-M form (MorleyHanfExtraction) was found false-shaped (statement audit 2026-07-07; see its docstring), so the sequence must come from a constructed model via the template / consistency-property route; this discharger applies there unchanged.

Absolute template truths on the Morley seed

The Morley seed's two members have sequence-independent template values: a sentence's tail template is its absolute truth in the model, and the disequality's is True for any pairwise distinct sequence. So the templates of ANY two pairwise-distinct sequences agree on the seed — which frees the realizing context's sequence from being a subsequence of the input.

theorem FirstOrder.Language.tailTemplateOfSeq_truth_sentence_iff {L : Language} {M : Type u_1} [L.Structure M] (c : ℕ → M) (φ : L.Sentenceω) : (tailTemplateOfSeq c).truth φ ↔ φ.Realize M

The tail template of any sequence assigns a sentence its absolute truth value (arity-0 formulas ignore the tuple).

theorem FirstOrder.Language.LocalEMContext.realizes_stage0_sentence_of_skolemUniversal (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (hsk : LocalSkolemUniversalForColim s₀) (ctx : (localColim s₀).LocalEMContext J) (hΓ : ΓEMlocal s₀ ⊆ ctx.Γ) (hc : OmegaCompleteForColim s₀ J ctx) (φ : s₀.Lang.Sentenceω) (hmem : ⟨0, φ⟩ ∈ Γlocal s₀ 0) (hφ : φ.Realize M) : φ.Realize (Carrier (localColim s₀) J ctx)

Stage-0 sentence satisfaction transfers to the carrier — the consumer-shaped bridge for the small-model assembly (issue #11 unit 7a): a stage-0 sentence of Γlocal s₀ 0 true in the source is true in the seed-language reduct of the context's carrier. Arity zero of the realization equivalence: tailTemplateOfSeq_truth_sentence_iff turns source truth into template truth, realize_templateSentence_localEM_iff_of_skolemUniversal transfers it to the carrier, and realize_templateSentence_of_structure removes the vacuous skeleton constants.

theorem FirstOrder.Language.tailTemplateOfSeq_truth_disEq {L : Language} {M : Type u_1} [L.Structure M] {c : ℕ → M} (hc : ∀ (i j : ℕ), i ≠ j → c i ≠ c j) : (tailTemplateOfSeq c).truth disEqFormula

The tail template of any pairwise distinct sequence declares the disequality true.

theorem FirstOrder.Language.morleySeed_template_agreement {L' : Language} {M : Type} [L'.Structure M] (φ : L'.Sentenceω) {a b : ℕ → M} (ha : ∀ (i j : ℕ), i ≠ j → a i ≠ a j) (hb : ∀ (i j : ℕ), i ≠ j → b i ≠ b j) (n : ℕ) (ψ : L'.BoundedFormulaω Empty n) : ⟨n, ψ⟩ ∈ Set.range (morleySeed φ) → ((tailTemplateOfSeq b).truth ψ ↔ (tailTemplateOfSeq a).truth ψ)

Morley-seed template agreement: the tail templates of any two pairwise-distinct sequences in the same model agree on Set.range (morleySeed φ) — the sentence member's value is absolute, and the disequality member's is True for both.

theorem FirstOrder.Language.morleySeed_template_agreement_cross {L' : Language} {M N : Type} [L'.Structure M] [L'.Structure N] (φ : L'.Sentenceω) {a : ℕ → M} {b : ℕ → N} (hφM : φ.Realize M) (hφN : φ.Realize N) (ha : ∀ (i j : ℕ), i ≠ j → a i ≠ a j) (hb : ∀ (i j : ℕ), i ≠ j → b i ≠ b j) (n : ℕ) (ψ : L'.BoundedFormulaω Empty n) : ⟨n, ψ⟩ ∈ Set.range (morleySeed φ) → ((tailTemplateOfSeq b).truth ψ ↔ (tailTemplateOfSeq a).truth ψ)

Cross-model Morley-seed template agreement: the seed construction does not require the two sequences to live in the same model — the tail templates of pairwise-distinct sequences in any two models both realizing the seed sentence agree on Set.range (morleySeed φ). This is the form the schema term model consumes (its sequence lives in the constructed quotient, not in the source).

theorem FirstOrder.Language.morleySeed_theory_model_of_isEmptyJ {L' : Language} {M : Type} [L'.Structure M] (φ : L'.Sentenceω) (a : ℕ → M) (J : Type) [LinearOrder J] [IsEmpty J] (hφreal : φ.Realize M) : ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model ((tailTemplateOfSeq a).templateTheoryOfSeq (morleySeed φ) J) N

The IsEmpty J degenerate case: over an empty target order, the Morley-seed template theory contains only the arity-0 (sentence) members, and the source model M itself realizes them — no EM construction needed.

Acceptance: tail-template realizability from the local EM model

theorem FirstOrder.Language.tailTemplateRealizable_of_localEMContext {L' : Language} [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] (s : ℕ → (n : ℕ) × L'.BoundedFormulaω Empty n) (M : Type) [L'.Structure M] [Nonempty M] (a : ℕ → M) (J : Type) [LinearOrder J] (ctx : (localColim (LocalStage.ofSeq L' s)).LocalEMContext J) : ΓEMlocal (LocalStage.ofSeq L' s) ⊆ ctx.Γ → LocalEMContext.OmegaCompleteForColim (LocalStage.ofSeq L' s) J ctx → (∀ (n : ℕ) (ψ : L'.BoundedFormulaω Empty n), ⟨n, ψ⟩ ∈ Set.range s → ((tailTemplateOfSeq ctx.a).truth ψ ↔ (tailTemplateOfSeq a).truth ψ)) → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model ((tailTemplateOfSeq a).templateTheoryOfSeq s J) N

Context-generic acceptance: any local EM context over the seed stage with ΓEMlocal-closure, support-covered Ω-completeness, and a template that agrees with the input's on Set.range s realizes the input's tail-template theory. The common core of the subsequence acceptance below (agreement from tailTemplateOfSeq_comp_truth_iff) and the full-indiscernibility wiring (agreement from the absolute Morley-seed values, morleySeed_template_agreement — no subsequence relation to the input needed).

theorem FirstOrder.Language.tailTemplateRealizable_of_localEMContext_cross {L' : Language} [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] (s : ℕ → (n : ℕ) × L'.BoundedFormulaω Empty n) {A : Type} [L'.Structure A] (a : ℕ → A) (Source : Type) [(localColim (LocalStage.ofSeq L' s)).Structure Source] (hsk : LocalSkolemUniversalForColim (LocalStage.ofSeq L' s)) (J : Type) [LinearOrder J] (ctx : (localColim (LocalStage.ofSeq L' s)).LocalEMContext J) : ΓEMlocal (LocalStage.ofSeq L' s) ⊆ ctx.Γ → LocalEMContext.OmegaCompleteForColim (LocalStage.ofSeq L' s) J ctx → (∀ (n : ℕ) (ψ : L'.BoundedFormulaω Empty n), ⟨n, ψ⟩ ∈ Set.range s → ((tailTemplateOfSeq ctx.a).truth ψ ↔ (tailTemplateOfSeq a).truth ψ)) → ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model ((tailTemplateOfSeq a).templateTheoryOfSeq s J) N

Cross-source acceptance: the context-generic acceptance with the context's source carrier separated from the input sequence's carrier — ctx.a lives in a mixin-satisfying Source (the schema term model), while the input a lives in an arbitrary L'-structure A (the large model). The template agreement hypothesis is the cross-model Morley-seed agreement's shape. The source's seed semantics are read through the seed-language reduct; no Nonempty Source is needed.

theorem FirstOrder.Language.tailTemplateRealizable_of_localEM {L' : Language} [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] (s : ℕ → (n : ℕ) × L'.BoundedFormulaω Empty n) (M : Type) [L'.Structure M] [Nonempty M] (a : ℕ → M) (J : Type) [LinearOrder J] (hTail : IsLomega1omegaIndiscernibleOnTail a (Set.range s)) (hOmega : ∃ (g : ℕ ↪o ℕ) (ctx : (localColim (LocalStage.ofSeq L' s)).LocalEMContext J), ctx.a = a ∘ ⇑g ∧ ctx.Γ = ΓEMlocal (LocalStage.ofSeq L' s) ∧ LocalEMContext.OmegaCompleteForColim (LocalStage.ofSeq L' s) J ctx) : ∃ (N : Type) (x : (L'.withConstants J).Structure N), Theoryω.Model ((tailTemplateOfSeq a).templateTheoryOfSeq s J) N

Per-s tail-template realizability via the local EM construction (the acceptance lemma): given the input sequence's tail indiscernibility on Set.range s and, for that s, the hypothesis hOmega — an extracted subsequence context over localColim (LocalStage.ofSeq L' s) that is OmegaCompleteForColim — the tail-template theory of a over any target order J has a model.

This lemma is hypothesis-relative and true for every s; what is not claimed is that hOmega is dischargeable for arbitrary s — its ∀-s closure is false-shaped (see the file docstring; a {Pᵢ} ∪ {⋀ᵢ Pᵢ} seed against a height model defeats any extraction). The honest instantiation is at s := morleySeed φ (MorleySeedOmegaExtraction). Every conjunct of hOmega except ctx.OmegaCompleteForColim is proved by exists_localEMContext_subseq. The extracted context's template agrees with the input's on the seed family (tailTemplateOfSeq_comp_truth_iff — this is why hOmega demands ctx.a = a ∘ g for an order embedding g, rather than an unrelated extracted sequence), so the model of the extracted template theory is a model of a's.

def FirstOrder.Language.MorleySeedOmegaExtraction (L' : Language) [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] : Prop

The seed Ω-residual, named: for the Morley-seed setup — sentence φ holding in the large source model M, input sequence a pairwise distinct and tail-indiscernible on Set.range (morleySeed φ), target order J — there is an extracted subsequence context (ctx.a = a ∘ g, ctx.Γ = ΓEMlocal) that is ΓlocalColim-restricted ⋁/⋀-complete.

Deliberately seed-specific and source-aware: the ∀-s closure of the acceptance bundle is false-shaped (see TailTemplateRealizable's docstring in Conditional/MorleyHanfTransfer.lean — a seed enumerating {Pᵢ x}ᵢ ∪ {⋀ᵢ Pᵢ x} against a height model defeats any extraction), so the residual carries exactly the facts the Morley–Hanf bridge actually has, including the ℶ_{ω₁} premise, all available to the future combinatorial proof. Every conjunct except OmegaCompleteForColim is already proved without them (exists_localEMContext_subseq). The downstream Conditional-facing morleySeedTailTemplateRealizable_of_localEMOmega shows this residual implies MorleySeedTailTemplateRealizable (modulo the extra function-symbol countability of this bridge).

WARNING — REFUTED (not_morleySeedOmegaExtraction_height, LocalEMOmegaResidual.lean): even seed-specific and source-aware, this bundle is false — the height pattern hides inside the true seed sentence ∃x, ¬⋀ᵢ Pᵢ(x), whose subformula closure re-imports the divergent conjunction into ΓlocalColim. Kept as the historical bundle shape; the honest residual must sit below OmegaCompleteForColim.

Equations

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

def FirstOrder.Language.MorleySeedOmegaHomogeneousExtraction (L' : Language) [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] : Prop

The seed homogeneity residual — the final frontier in its cleanest form: for the Morley-seed setup there is a subsequence a ∘ g that is tail-indiscernible on ΓEMlocal and source-side Ω-homogeneous (LocalEMOmegaHomogeneous). J-free — the target order enters only downstream, through omegaCompleteForColim_of_omegaHomogeneous, for every J at once. Seed-specific and source-aware like MorleySeedOmegaExtraction (whose docstring records why the ∀-s form is false-shaped); the ℶ_{ω₁} and φ-realization facts are available to the future combinatorial proof. The plain Ramsey extraction (exists_orderEmb_tailIndiscernible_ΓEMlocal) already achieves the first conjunct; the remaining content is the second — a countable-family homogeneity statement about eventual truth of the de-substituted seed-family formulas on consecutive (a ∘ g)-tuples, with no term model, no quotients, no supports.

WARNING — REFUTED (not_morleySeedOmegaHomogeneousExtraction_height, LocalEMOmegaResidual.lean): the uniform iInf-cutoff clause fails for every subsequence of the height sequence once the divergent conjunction hides inside a true seed sentence. Kept as the historical clean form; see LocalEMOmegaResidual.lean for the audit and the reshape direction.

Equations

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

theorem FirstOrder.Language.morleySeedOmegaExtraction_of_homogeneousExtraction {L' : Language} [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] (h : L'.MorleySeedOmegaHomogeneousExtraction) : L'.MorleySeedOmegaExtraction

The seed homogeneity residual discharges the seed Ω-residual: a homogeneous extraction yields, for every target order J, the subsequence context bundle — the context is the canonical one over a ∘ g (as in exists_localEMContext_subseq), and its OmegaCompleteForColim comes from the reduction theorem omegaCompleteForColim_of_omegaHomogeneous.