The schema term model as a local-EM source #
The integration point of the schema route with the (now generic) local-EM truth-lemma chain: the
schema term model satisfies the FULL arbitrary-stage Skolem-universality mixin
LocalSkolemUniversalForColim — no weakening to successor stages is needed.
The subtle point is a raw-stage membership ⟨n, .all ψ⟩ ∈ Γlocal s₀ k: the body ψ itself need
not lie in Γlocal s₀ k (stage 0 is not subformula closed), so the restricted truth lemma
cannot be applied to it directly. The route is liftNegBody_mem_Γlocal_succ: the lifted negated
body (ψ.not).mapLanguage (LlocalHom s₀ k) IS controlled one stage up. Truth of ψ at the
stage-k Skolem value (the class of locSkWitnessTerm) makes the lifted negated body false in
the quotient; completeness pins its negation in the completion; and if the universal sentence
were negative, one two-sentence Marker body would realize both signs — under the body's
interpretation, locSkWitness_universal_constInterp_nat turns the first fact into the universal,
a contradiction. The universal sentence is therefore positive, and the truth lemma reads it back
into the quotient.
The schema term model satisfies the Skolem-universality mixin — the full arbitrary-stage
form. This is what plugs the schema term model into the generic local-EM truth lemma
(truthLemmaStage_of_skolemUniversal) and the cross-source acceptance.
The arbitrary-order local-EM context over the schema term model #
Section-9 scaffolding: for ANY target linear order J, the schema term model carries a
LocalEMContext whose sequence is schemaSeq, whose family is ΓEMlocal, and whose
Ω-completeness is exactly the discharged TailTemplateOmegaWitnessed — plus the seed-sentence
realization the Morley-seed agreement consumes.
The schema local-EM context over an arbitrary target order J: sequence schemaSeq,
family ΓEMlocal, tail indiscernibility from the full (cutoff-0) indiscernibility, atoms by
the ΓEMlocal dischargers.
Equations
- FirstOrder.Language.schemaTermLocalEMContext hM J = { a := FirstOrder.Language.schemaSeq hM, Γ := FirstOrder.Language.ΓEMlocal s₀, hind := ⋯, atom_mem := ⋯, rel_mem := ⋯ }
Instances For
The schema context is Ω-complete — the discharged TailTemplateOmegaWitnessed
(the completion's pinned iSup/negative-iInf witnesses) converted through the Layer-7a
bridge.
Seed-sentence realization: a stage-0 family sentence true in the source M is realized
by the schema term model (in its seed-language reduct). The route: validity of its lifted
template under every body interpretation forces the positive sign; the sequence-realization
bridge reads it into the quotient; the seed reduct peels off LlocalInclusion.
The Morley-seed tail-template model (the section-9 assembly) #
The schema route's endpoint: for a sentence φ true in a source of size ≥ ℶ_{ω₁} and ANY
target linear order J, the Morley-seed tail-template theory of any pairwise-distinct source
sequence has a model — the schema term model's quotient, through the cross-source acceptance.
No tail indiscernibility of the input sequence is consumed: the seed's template values are
absolute (morleySeed_template_agreement_cross), so the input sequence only contributes its
pairwise distinctness. This discharges the honest residual
MorleySeedTailTemplateRealizable (the source facts it carries are exactly these).
The Morley-seed tail-template theory has a model over every target order — assembled
from: a well-ordering of the source (exists_wellFoundedLT), the schema completion over
LocalStage.ofSeq L' (morleySeed φ), the schema context and its Ω-completeness, the seed
realization + pairwise distinctness feeding the cross-model seed agreement, and the cross-source
acceptance with the schema term model's Skolem-universality mixin.