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.realize_term_mkClass (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (ts : Fin n → (Λ.withConstants J).Term Empty) (t : (Λ.withConstants J).Term (Empty ⊕ Fin n)) : Term.realize (Sum.elim Empty.elim fun (i : Fin n) => mkClass Λ J ctx (ts i)) t = mkClass Λ J ctx (t.subst (Sum.elim (fun (e : Empty) => e.elim) ts))

Carrier-side term substitution: realizing a term in the local EM term model under the assignment Sum.elim Empty.elim (mkClass ∘ ts) gives the class of the substituted closed term. By induction on the term, using funMap_mkClass. Local analogue of EMContext.realize_term_mkClass.

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.eventually_imp_iff_imp_eventually {α : Type u_1} {f : Filter α} {P Q : α → Prop} (hP : (∀ᶠ (x : α) in f, P x) ∨ ∀ᶠ (x : α) in f, ¬P x) : (∀ᶠ (x : α) in f, P x → Q x) ↔ (∀ᶠ (x : α) in f, P x) → ∀ᶠ (x : α) in f, Q x

An eventual implication splits as an implication of eventuals exactly when the antecedent's eventual truth is decided. The Filter fact behind the truth lemma's imp case — only the antecedent's decidedness is needed.

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.

theorem FirstOrder.Language.locDeepInterp_skWitness (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [s₀.Lang.Structure M] [Nonempty M] (a : ℕ → M) (d : ℕ) (S : Finset 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₀).locDeepInterp J a d S (locSkWitnessTerm s₀ J h ts) = Classical.epsilon fun (b : M) => ψ.not.Realize Empty.elim (Fin.snoc (fun (i : Fin n) => (localColim s₀).locDeepInterp J a d S (ts i)) b)

Deep value of the local Skolem-witness term: it is exactly the Hilbert-choice value for ¬ψ on the deep interpretations of the arguments (read in the source model's stage-k structure). The localColimStructure/localStageStructure/localSkolemStructure funMap coherence is fully definitional, so this is rfl after the term/funMap unfolding. Local analogue of deepInterp_skWitness.

theorem FirstOrder.Language.locSkWitness_universal (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [s₀.Lang.Structure M] [Nonempty M] (a : ℕ → M) (d : ℕ) (S : Finset 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) : (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ k) ψ).Realize Empty.elim (Fin.snoc (fun (i : Fin n) => (localColim s₀).locDeepInterp J a d S (ts i)) ((localColim s₀).locDeepInterp J a d S (locSkWitnessTerm s₀ J h ts))) → ∀ (x : M), (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ k) ψ).Realize Empty.elim (Fin.snoc (fun (i : Fin n) => (localColim s₀).locDeepInterp J a d S (ts i)) x)

Local Skolem-witness universality (the contrapositive Skolem axiom, transported to the deep tuple): if the body ψ holds at the deep interpretation of its Skolem-witness term (for ¬ψ), then it holds at every M-element. The Skolem input consumed inline by the all case of the local truth lemma. Local analogue of skWitness_universal.