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 }

Skeleton-constant terms: support and deep interpretation

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.

3. Template preservation under subsequence

4. The parameterized EM model theorem

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.

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