The local EM truth lemma, layer 1: truth kernel + Skolem-witness transport

This file assembles the pieces the restricted local truth lemma consumes, in two parts.

The generic truth kernel (section TruthKernel, over any [Λ.Structure M]): the eventual-deep- truth predicate LocalEMContext.eventualDeepTruth, the carrier substitution bridge realize_term_mkClass, the atom cases eventualDeepTruth_equal_iff/_rel_iff, the 0-1 decidedness law eventualDeepTruth_decided, the imp/falsum connective cases (eventually_imp_iff_imp_eventually, eventualDeepTruth_falsum_iff, eventualDeepTruth_imp_iff), and the all-case class/snoc bridge mkClass_snoc. Ported from EMTermModel.lean:820–1115. These are generic over Λ (they touch only the generic quotient structure + realize bridges), so no localColim-specific plumbing is needed.

The Skolem-witness transport (section WitnessTransport, over localColim s₀): the restricted truth lemma's all case (∀ψ) needs, in the source model, the Hilbert-choice witness of ¬ψ as an actual closed term of (localColim s₀)[[J]], together with the semantic "witness universality" it delivers. This part builds exactly that transport, mirroring the skWitnessTerm/deepInterp_skWitness/skWitness_universal chain of EMTermModel.lean but over the countable local tower:

• locSkWitnessTerm — the colimit-level witness term for a stage-k universal ∀ψ ∈ Γlocal s₀ k, built from the local Skolem symbol skolemNeedSymbol h (witnessing ∃ xₙ, ¬ψ), included through LlocalInclusion s₀ (k+1) and then lhomWithConstants;
• locJSupport_locSkWitnessTerm — its head is an L-function symbol, not a J-constant, so its J-support is just the union of the arguments';
• locDeepInterp_skWitness — its deep interpretation is exactly the Hilbert-choice value for ¬ψ on the deep interpretations of the arguments (the localColimStructure/localStageStructure/ localSkolemStructure funMap coherence is fully definitional, so this is rfl after unfolding);
• locSkWitness_universal — the Skolem-axiom transport: if ψ holds at the deep tuple extended by the witness's deep value, then it holds at every M-element. Powered by localSkolem_funMap_spec (in LocalSkolem.lean) and the realization transport realize_map_LlocalInclusion.

This is the local analogue of EMTermModel.lean:114–180. It is a pure file (imports LocalEMContext, not the Conditional-touching LocalEMExtraction) so the local context/truth stack stays off the EM stack.

The generic truth kernel

The atom/connective rewrite API and the eventual-deep-truth decidedness fact, generic over any [Λ.Structure M] (they only touch the generic quotient structure of LocalEMContext.lean plus the realize_locDeForm/locDeepInterp_onTerm_subst bridges — no localColim-specific plumbing). The OmegaComplete mixin, TLReady, and the staged induction are later layers.

def FirstOrder.Language.LocalEMContext.eventualDeepTruth (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (φ : Λ.BoundedFormulaω Empty n) (ts : Fin n → (Λ.withConstants J).Term Empty) (S : Finset J) : Prop

Eventual deep truth of a base-language formula φ on a tuple of closed argument terms over a support S: φ holds in M on the deep interpretations of the terms, for all sufficiently deep d. The right-hand side of the restricted truth lemma. Local analogue of EMContext.eventualDeepTruth.

Equations

• FirstOrder.Language.LocalEMContext.eventualDeepTruth Λ J ctx φ ts S = ∀ᶠ (d : ℕ) in Filter.atTop, φ.Realize Empty.elim fun (i : Fin n) => Λ.locDeepInterp J ctx.a d S (ts i)

theorem FirstOrder.Language.LocalEMContext.eventualDeepTruth_equal_iff (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (t₁ t₂ : Λ.Term (Empty ⊕ Fin n)) (ts : Fin n → (Λ.withConstants J).Term Empty) {S : Finset J} (hS : Λ.locJSupport J (((Λ.lhomWithConstants J).onTerm t₁).subst (Sum.elim (fun (e : Empty) => e.elim) ts)) ∪ Λ.locJSupport J (((Λ.lhomWithConstants J).onTerm t₂).subst (Sum.elim (fun (e : Empty) => e.elim) ts)) ⊆ S) : ((BoundedFormulaω.mapLanguage (Λ.lhomWithConstants J) (BoundedFormulaω.equal t₁ t₂)).Realize Empty.elim fun (i : Fin n) => mkClass Λ J ctx (ts i)) ↔ eventualDeepTruth Λ J ctx (BoundedFormulaω.equal t₁ t₂) ts S

Truth lemma, equality-atom case: realizing a base-language equality atom in the local EM term model on a tuple of term-classes is equivalent to its eventual deep truth. Carrier side via realize_term_mkClass; quotient side via Quotient.eq; deep side via eventually_locDeepInterp_superset_iff and locDeepInterp_onTerm_subst.

theorem FirstOrder.Language.LocalEMContext.eventualDeepTruth_rel_iff (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n l : ℕ} (R : Λ.Relations l) (args : Fin l → Λ.Term (Empty ⊕ Fin n)) (ts : Fin n → (Λ.withConstants J).Term Empty) {S : Finset J} (hS : (Finset.univ.biUnion fun (i : Fin l) => Λ.locJSupport J (((Λ.lhomWithConstants J).onTerm (args i)).subst (Sum.elim (fun (e : Empty) => e.elim) ts))) ⊆ S) : ((BoundedFormulaω.mapLanguage (Λ.lhomWithConstants J) (BoundedFormulaω.rel R args)).Realize Empty.elim fun (i : Fin n) => mkClass Λ J ctx (ts i)) ↔ eventualDeepTruth Λ J ctx (BoundedFormulaω.rel R args) ts S

Truth lemma, relation-atom case: realizing a base-language relation atom in the local EM term model on a tuple of term-classes is equivalent to its eventual deep truth. Carrier side via realize_term_mkClass; then relMap_mkClass_iff; deep side via locDeepInterp_onTerm_subst.

theorem FirstOrder.Language.LocalEMContext.eventualDeepTruth_decided (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (φ : Λ.BoundedFormulaω Empty n) (ts : Fin n → (Λ.withConstants J).Term Empty) (S : Finset J) (hsub : ∀ (i : Fin n), Λ.locJSupport J (ts i) ⊆ S) (hmem : ⟨S.card, Λ.locDeForm J S φ ts hsub⟩ ∈ ctx.Γ) : (∀ᶠ (d : ℕ) in Filter.atTop, φ.Realize Empty.elim fun (i : Fin n) => Λ.locDeepInterp J ctx.a d S (ts i)) ∨ ∀ᶠ (d : ℕ) in Filter.atTop, ¬φ.Realize Empty.elim fun (i : Fin n) => Λ.locDeepInterp J ctx.a d S (ts i)

0-1 law for eventual deep truth (the unlock for the truth lemma's imp/connective cases): if the de-substituted formula locDeForm S φ ts lies in the tail-indiscernible family Γ, then φ's eventual deep truth is decided. The value is eventually constant because tail indiscernibility makes all sufficiently-deep consecutive tuples agree on the single arity-S.card formula. Local analogue of EMContext.eventualDeepTruth_decided.

theorem FirstOrder.Language.LocalEMContext.eventualDeepTruth_falsum_iff (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (ts : Fin n → (Λ.withConstants J).Term Empty) (S : Finset J) : eventualDeepTruth Λ J ctx BoundedFormulaω.falsum ts S ↔ False

Truth lemma, falsum case (eventual-deep-truth side): falsum has no eventual deep truth. Immediate from Filter.eventually_const (atTop on ℕ is NeBot).

theorem FirstOrder.Language.LocalEMContext.eventualDeepTruth_imp_iff (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (φ ψ : Λ.BoundedFormulaω Empty n) (ts : Fin n → (Λ.withConstants J).Term Empty) (S : Finset J) (hdec : (∀ᶠ (d : ℕ) in Filter.atTop, φ.Realize Empty.elim fun (i : Fin n) => Λ.locDeepInterp J ctx.a d S (ts i)) ∨ ∀ᶠ (d : ℕ) in Filter.atTop, ¬φ.Realize Empty.elim fun (i : Fin n) => Λ.locDeepInterp J ctx.a d S (ts i)) : eventualDeepTruth Λ J ctx (φ.imp ψ) ts S ↔ eventualDeepTruth Λ J ctx φ ts S → eventualDeepTruth Λ J ctx ψ ts S

Truth lemma, imp case (eventual-deep-truth side): the eventual deep truth of φ ⟹ ψ is the implication of their eventual deep truths, provided φ's eventual deep truth is decided (supplied by eventualDeepTruth_decided). Local analogue of EMContext.eventualDeepTruth_imp_iff.

theorem FirstOrder.Language.LocalEMContext.mkClass_snoc (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {m : ℕ} (ts : Fin m → (Λ.withConstants J).Term Empty) (u : (Λ.withConstants J).Term Empty) : Fin.snoc (fun (i : Fin m) => mkClass Λ J ctx (ts i)) (mkClass Λ J ctx u) = fun (i : Fin (m + 1)) => mkClass Λ J ctx (Fin.snoc ts u i)

Forming classes commutes with Fin.snoc: the carrier tuple obtained by snocing mkClass u onto mkClass ∘ ts is mkClass ∘ (Fin.snoc ts u). The bridge between the carrier-side ∀x (over term-classes) and the term-side Fin.snoc ts u in the all case. Local analogue of EMContext.mkClass_snoc.

Local Skolem-witness transport (over localColim s₀)

def FirstOrder.Language.locSkWitnessTerm (s₀ : LocalStage) (J : Type) {k n : ℕ} {ψ : (Llocal s₀ k).BoundedFormulaω Empty (n + 1)} (h : ⟨n, ψ.all⟩ ∈ Γlocal s₀ k) (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) : ((localColim s₀).withConstants J).Term Empty

The colimit-level local Skolem-witness term for a stage-k universal ∀ψ ∈ Γlocal s₀ k: the local Skolem symbol skolemNeedSymbol h (witnessing ∃ xₙ, ¬ψ), in the localSkolem summand of Llocal s₀ (k+1), included through LlocalInclusion s₀ (k+1) and then lhomWithConstants, applied to the closed argument terms ts. Local analogue of skWitnessTerm.

Equations

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

theorem FirstOrder.Language.locJSupport_locSkWitnessTerm (s₀ : LocalStage) (J : Type) [LinearOrder J] {k n : ℕ} {ψ : (Llocal s₀ k).BoundedFormulaω Empty (n + 1)} (h : ⟨n, ψ.all⟩ ∈ Γlocal s₀ k) (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) : (localColim s₀).locJSupport J (locSkWitnessTerm s₀ J h ts) = Finset.univ.biUnion fun (i : Fin n) => (localColim s₀).locJSupport J (ts i)

The witness term mentions only the J-constants of its arguments (its head is an L-function symbol, not a skeleton constant), so its support is covered whenever the arguments' is. Local analogue of jSupport_skWitnessTerm.