The local EM context, layer 1: deep interpretation and realize bridges

The semantic layer of the EMContext re-base, generic over Λ: the deep interpretation of closed Λ[[J]]-terms in a source model and the realize bridges connecting it to the syntactic de-substitution pipeline of LocalEMFamily.lean. Mirrors the skolemColim-specific chain of EMTermModel.lean, with one systematic simplification: every original proof touched the language structure only through letI := skolemColimStructure L, so here the structure is simply the ambient instance [Λ.Structure M] — localColimStructure enters only at instantiation sites (as in LocalEMExtraction.lean). No [Nonempty M] is needed (no Hilbert choice in this layer).

Contents (source lemma in EMTermModel.lean in parentheses):

• locDeepInterp (deepInterp) + locDeepInterp_func, and the realization bridges locDeepInterp_eq_realize, locDeepInterp_subst, locDeepInterp_onTerm_subst;
• the support bridge locJSupport_onTerm_subst_subset (jSupport_onTerm_subst_subset);
• the ordered-position/Fin-arity bridges locDeepInterp_eq_realize_pos, locDeTermFin_realize (deepInterp_eq_realize_fin), and the superset realization invariance locDeTermFin_realize_superset;
• the atom bridges realize_locDeEqAtom(_superset), realize_locDeRelAtom(_superset) — the superset variants route through locDeTermFin_realize_superset instead of re-deriving the per-term key inline as the originals do;
• the general formula bridge realize_locDeForm (realize_deForm), consuming realize_openBounds (imported explicitly from Methods/Henkin/Construction.lean) and realize_relabel_sumInr_zero (from the Lomega1omega core).

This file also carries the generic quotient layer: locDeepInterp_snoc, the eventual-equality relation LocalEMEq (refl/symm) with its support-enlargement engine (LocalEMEq_eventually_on_superset, eventually_locDeepInterp_superset_iff, eventually_locRelMap_superset_iff), the LocalEMContext standing-data structure, and (in the Quotient section) the carrier + Λ[[J]]-Structure. The tail-indiscernibility predicate IsLomega1omegaIndiscernibleOnTail comes from the neutral Methods/TailIndiscernible.lean, so this file stays EM-free.

Next layers (subsequent chunks): the skolemNeedSymbol witness-term transport and the family-membership-carrying restricted truth lemma.

Support of substituted base-language terms (syntactic)

theorem FirstOrder.Language.locJSupport_onTerm_subst_subset (Λ : Language) (J : Type) [LinearOrder J] {n : ℕ} (t : Λ.Term (Empty ⊕ Fin n)) (ts : Fin n → (Λ.withConstants J).Term Empty) : Λ.locJSupport J (((Λ.lhomWithConstants J).onTerm t).subst (Sum.elim (fun (e : Empty) => e.elim) ts)) ⊆ Finset.univ.biUnion fun (i : Fin n) => Λ.locJSupport J (ts i)

Support of a base-language term after substitution: substituting the closed terms ts for the free variables of a base-language term (onTerm t) (which itself carries no J-constants, being a Λ-image) produces only the J-constants of the ts. The bridge from a uniform support hypothesis S ⊇ ⋃ locJSupport (ts i) to the per-atom support hypotheses of the congruence layer.

Deep interpretation

noncomputable def FirstOrder.Language.locDeepInterp (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (d : ℕ) (S : Finset J) (t : (Λ.withConstants J).Term Empty) : M

The deep interpretation of a closed Λ[[J]]-term at depth d relative to a support S: interpret each J-constant c_j by the source sequence at position d + deepRank S j (so support constants map to a strictly-increasing deep tuple of a), and evaluate in M's ambient Λ-structure.

Equations

• Λ.locDeepInterp J a d S t = FirstOrder.Language.Term.realize Empty.elim t

theorem FirstOrder.Language.locDeepInterp_func (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (d : ℕ) (S : Finset J) {n : ℕ} (f : (Λ.withConstants J).Functions n) (ts : Fin n → (Λ.withConstants J).Term Empty) : Λ.locDeepInterp J a d S (func f ts) = Structure.funMap f fun (i : Fin n) => Λ.locDeepInterp J a d S (ts i)

Deep interpretation commutes with function application (same depth and support): it is the structure's funMap of the argument interpretations. Immediate from Term.realize.

theorem FirstOrder.Language.locDeepInterp_eq_realize (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (d : ℕ) (S : Finset J) (t : (Λ.withConstants J).Term Empty) : Λ.locDeepInterp J a d S t = Term.realize (Sum.elim (fun (j : J) => a (d + deepRank J S j)) Empty.elim) t.constantsToVars

De-substitution bridge: the deep interpretation of a closed term equals the de-substituted Λ-term constantsToVars t (each skeleton constant c_j turned into the variable Sum.inl j) realized with j ↦ a (d + deepRank S j). Turns the support machinery from combinatorial into semantic — the right-hand side is a genuine formula realization, so tail indiscernibility applies.

theorem FirstOrder.Language.locDeepInterp_onTerm_subst (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (d : ℕ) (S : Finset J) {n : ℕ} (t : Λ.Term (Empty ⊕ Fin n)) (ts : Fin n → (Λ.withConstants J).Term Empty) : Λ.locDeepInterp J a d S (((Λ.lhomWithConstants J).onTerm t).subst (Sum.elim (fun (e : Empty) => e.elim) ts)) = Term.realize (Sum.elim Empty.elim fun (i : Fin n) => Λ.locDeepInterp J a d S (ts i)) t

Deep interpretation of a base-language substituted term: combining locDeepInterp_subst with realize_onTerm, the deep interpretation of (onTerm t).subst ts equals t realized in M's ambient Λ-structure on the deep interpretations of the substituted terms.

Ordered-position and Fin-arity realize bridges

theorem FirstOrder.Language.locDeTermFin_realize (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (d : ℕ) (S : Finset J) (t : (Λ.withConstants J).Term Empty) (hsub : Λ.locJSupport J t ⊆ S) : Λ.locDeepInterp J a d S t = Term.realize (fun (i : Fin S.card) => a (d + ↑i)) (Λ.locDeTermFin J S t hsub)

Fin-arity realize bridge: the deep interpretation is the realize of the Fin S.card-indexed de-substituted term on the consecutive deep tuple i ↦ a (d + i), directly feeding the atoms.

theorem FirstOrder.Language.locDeTermFin_realize_superset (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (d : ℕ) (S T : Finset J) (w : (Λ.withConstants J).Term Empty) (hw : Λ.locJSupport J w ⊆ S) : Term.realize (fun (i : Fin S.card) => a (d + deepRank J T ((S.orderEmbOfFin ⋯) i))) (Λ.locDeTermFin J S w hw) = Λ.locDeepInterp J a d T w

Superset realization invariance: the Fin-arity de-substituted term over S, realized on the T-induced deep tuple i ↦ a (d + deepRank T (orderEmbOfFin S i)), equals the deep interpretation over the larger support T. The core shared by the equality- and relation-atom superset bridges (restrictVar realize with a dite-extended assignment, then realize_eq_of_eq_on_varFinset to discard the junk, then orderEmbOfFin_deepRank).

Atom and formula realize bridges

theorem FirstOrder.Language.realize_locDeForm (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (d : ℕ) (S : Finset J) {n : ℕ} (φ : Λ.BoundedFormulaω Empty n) (ts : Fin n → (Λ.withConstants J).Term Empty) (hsub : ∀ (i : Fin n), Λ.locJSupport J (ts i) ⊆ S) : ((Λ.locDeForm J S φ ts hsub).Realize Empty.elim fun (i : Fin S.card) => a (d + ↑i)) ↔ φ.Realize Empty.elim fun (i : Fin n) => Λ.locDeepInterp J a d S (ts i)

General formula realize bridge (generalizes the atom bridges): the local de-substituted formula holds on the consecutive deep tuple i ↦ a (d + i) iff φ holds in M's ambient Λ-structure on the deep interpretations of ts at depth d over S.

theorem FirstOrder.Language.locDeepInterp_snoc (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (d : ℕ) (S : Finset J) {n : ℕ} (ts : Fin n → (Λ.withConstants J).Term Empty) (u : (Λ.withConstants J).Term Empty) : (fun (i : Fin (n + 1)) => Λ.locDeepInterp J a d S (Fin.snoc ts u i)) = Fin.snoc (fun (i : Fin n) => Λ.locDeepInterp J a d S (ts i)) (Λ.locDeepInterp J a d S u)

Deep interpretation commutes with Fin.snoc: interpreting the one-point extension Fin.snoc ts u gives the snoc of the interpretations. Semantic prep for the later truth lemma's all case (relating the carrier's ∀x over term-classes to the body's argument tuple).

Eventual deep equality LocalEMEq and the support-enlargement engine

def FirstOrder.Language.LocalEMEq (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (t u : (Λ.withConstants J).Term Empty) : Prop

Eventual deep equality: closed terms t, u are identified when, for all sufficiently deep interpretations of their combined skeleton support, they evaluate equally in M. (The combined support means both terms are read against the same ordered finite skeleton.)

Equations

• Λ.LocalEMEq J a t u = ∀ᶠ (d : ℕ) in Filter.atTop, Λ.locDeepInterp J a d (Λ.locJSupport J t ∪ Λ.locJSupport J u) t = Λ.locDeepInterp J a d (Λ.locJSupport J t ∪ Λ.locJSupport J u) u

theorem FirstOrder.Language.LocalEMEq.refl (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) (t : (Λ.withConstants J).Term Empty) : Λ.LocalEMEq J a t t

theorem FirstOrder.Language.LocalEMEq.symm (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) {t u : (Λ.withConstants J).Term Empty} (h : Λ.LocalEMEq J a t u) : Λ.LocalEMEq J a u t

theorem FirstOrder.Language.eventually_locDeepInterp_superset_iff (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (a : ℕ → M) {Γ : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)} (hind : IsLomega1omegaIndiscernibleOnTail a Γ) {t u : (Λ.withConstants J).Term Empty} (hmem : ⟨(Λ.locJSupport J t ∪ Λ.locJSupport J u).card, Λ.locDeEqAtom J (Λ.locJSupport J t ∪ Λ.locJSupport J u) t u ⋯ ⋯⟩ ∈ Γ) {S : Finset J} (hS : Λ.locJSupport J t ∪ Λ.locJSupport J u ⊆ S) : ∀ᶠ (d : ℕ) in Filter.atTop, Λ.locDeepInterp J a d (Λ.locJSupport J t ∪ Λ.locJSupport J u) t = Λ.locDeepInterp J a d (Λ.locJSupport J t ∪ Λ.locJSupport J u) u ↔ Λ.locDeepInterp J a d S t = Λ.locDeepInterp J a d S u

Support-enlargement iff (the symmetric core): on the deep tail the deep equality over the combined support S₀ is equivalent to the deep equality over any larger support S ⊇ S₀. Both directions — descending from a larger support back to S₀ is what LocalEMContext.trans needs.

The local EM quotient context

To avoid threading the indiscernible sequence, its tail-indiscernible family, and the atomic-diagram membership through every congruence proof, we bundle them in a LocalEMContext. Every quotient operation then uses LocalEMEq_eventually_on_superset (via the support-enlargement iff) as its standing congruence engine. Generic over Λ and [Λ.Structure M]; the countable local instance is built in LocalEMExtraction.lean.

structure FirstOrder.Language.LocalEMContext (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] : Type

The standing data for the local EM quotient over a fixed source model M: a sequence a of deep indiscernibles, a tail-indiscernible family Γ, and the fact that every de-substituted atom lies in Γ. The structure accepts an arbitrary Γ; the countable local family ΓEMlocal and its tail-indiscernible sequence discharge these fields at instantiation (LocalEMExtraction.lean).

• a : ℕ → M

  The deep indiscernible sequence.

• Γ : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)

  The tail-indiscernible formula family.

• hind : IsLomega1omegaIndiscernibleOnTail self.a self.Γ

  Tail indiscernibility of a on Γ.

• atom_mem (S : Finset J) (t u : (Λ.withConstants J).Term Empty) (ht : Λ.locJSupport J t ⊆ S) (hu : Λ.locJSupport J u ⊆ S) : ⟨S.card, Λ.locDeEqAtom J S t u ht hu⟩ ∈ self.Γ

  Every de-substituted equality atom is in Γ.

• rel_mem (S : Finset J) {l : ℕ} (R : Λ.Relations l) (ts : Fin l → (Λ.withConstants J).Term Empty) (ht : ∀ (i : Fin l), Λ.locJSupport J (ts i) ⊆ S) : ⟨S.card, Λ.locDeRelAtom J S R ts ht⟩ ∈ self.Γ

  Every de-substituted relation atom is in Γ.

theorem FirstOrder.Language.locJSupport_subterm (Λ : Language) (J : Type) [LinearOrder J] {α : Type} {n : ℕ} (f : (Λ.withConstants J).Functions n) (ts : Fin n → (Λ.withConstants J).Term α) (i : Fin n) : Λ.locJSupport J (ts i) ⊆ Λ.locJSupport J (func f ts)

Support monotonicity: an argument's skeleton support is contained in the whole term's.

theorem FirstOrder.Language.LocalEMContext.trans (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {t u v : (Λ.withConstants J).Term Empty} (h1 : Λ.LocalEMEq J ctx.a t u) (h2 : Λ.LocalEMEq J ctx.a u v) : Λ.LocalEMEq J ctx.a t v

Transitivity of LocalEMEq (the congruence engine's first payoff): enlarge to the union of all three supports, transport both hypotheses up to it via the enlargement iff, chain the equalities in M, and descend back to the (t,v)-support.

theorem FirstOrder.Language.LocalEMContext.func_congr (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (f : (Λ.withConstants J).Functions n) {ts ts' : Fin n → (Λ.withConstants J).Term Empty} (h : ∀ (i : Fin n), Λ.LocalEMEq J ctx.a (ts i) (ts' i)) : Λ.LocalEMEq J ctx.a (func f ts) (func f ts')

Function congruence: if the arguments are pairwise LocalEMEq, so are the function terms. Enlarge every argument's deep equality up to the whole term's support, combine the finitely many eventual equalities, and apply locDeepInterp_func.

def FirstOrder.Language.LocalEMContext.setoid (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) : Setoid ((Λ.withConstants J).Term Empty)

LocalEMEq is an equivalence relation on closed terms (refl/symm need no context; trans is LocalEMContext.trans).

Equations

• FirstOrder.Language.LocalEMContext.setoid Λ J ctx = { r := Λ.LocalEMEq J ctx.a, iseqv := ⋯ }

def FirstOrder.Language.LocalEMContext.Carrier (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) : Type

The local EM term-model carrier for a context: closed Λ[[J]]-terms modulo LocalEMEq.

Equations

• FirstOrder.Language.LocalEMContext.Carrier Λ J ctx = Quotient (FirstOrder.Language.LocalEMContext.setoid Λ J ctx)

def FirstOrder.Language.LocalEMContext.mkClass (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (t : (Λ.withConstants J).Term Empty) : Carrier Λ J ctx

A closed term as an element of the carrier.

Equations

• FirstOrder.Language.LocalEMContext.mkClass Λ J ctx t = ⟦t⟧

@[reducible]

noncomputable def FirstOrder.Language.LocalEMContext.structure (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) : (Λ.withConstants J).Structure (Carrier Λ J ctx)

The local EM term-model structure on the carrier: function symbols act by term formation f([ts]) := [func f ts] (skeleton constants are the arity-0 case), and a relation holds iff it holds in M on the deep interpretations for all sufficiently deep d (read over a common support of the arguments). Well-definedness is proved separately via the enlargement-invariance congruence engine.

Equations

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

theorem FirstOrder.Language.LocalEMContext.funMap_mkClass (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (f : (Λ.withConstants J).Functions n) (ts : Fin n → (Λ.withConstants J).Term Empty) : (Structure.funMap f fun (i : Fin n) => mkClass Λ J ctx (ts i)) = mkClass Λ J ctx (func f ts)

Function interpretation computes on classes (well-definedness): applying the interpreted function symbol to a tuple of term-classes gives the class of the function term. Immediate from func_congr and Quotient.out_eq. (The arity-0 case is constMap_mkClass.)

theorem FirstOrder.Language.LocalEMContext.constMap_mkClass (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (c : (Λ.withConstants J).Functions 0) : Structure.funMap c Fin.elim0 = mkClass Λ J ctx (func c Fin.elim0)

The arity-0 case: a skeleton constant c_j (or any Λ-constant) interprets as the class of its constant term.

theorem FirstOrder.Language.LocalEMContext.relMap_mkClass_iff (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {l : ℕ} (R : Λ.Relations l) (ts : Fin l → (Λ.withConstants J).Term Empty) {S : Finset J} (hS : (Finset.univ.biUnion fun (i : Fin l) => Λ.locJSupport J (ts i)) ⊆ S) : (Structure.RelMap (Sum.inl R) fun (i : Fin l) => mkClass Λ J ctx (ts i)) ↔ ∀ᶠ (d : ℕ) in Filter.atTop, Structure.RelMap R fun (i : Fin l) => Λ.locDeepInterp J ctx.a d S (ts i)

Relation interpretation computes on classes (well-definedness): the interpreted relation holds on a tuple of term-classes iff it holds in M on the deep interpretations for all sufficiently deep d, over any support S covering the arguments — independent of the representatives and of the chosen support. The relation analogue of funMap_mkClass, via a bridge support T = S ∪ Sout.

@[reducible]

noncomputable def FirstOrder.Language.LocalEMContext.structureBase (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) : Λ.Structure (Carrier Λ J ctx)

The base Λ-structure on the carrier: the reduct of the term-model [[J]]-structure along the skeleton-constant inclusion (a base function/relation symbol acts as its Sum.inl image).

Equations

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

theorem FirstOrder.Language.LocalEMContext.lhomWithConstants_isExpansionOn (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) : (Λ.lhomWithConstants J).IsExpansionOn (Carrier Λ J ctx)

Map-language plumbing: the skeleton-constant inclusion Λ → Λ[[J]] is an expansion of the carrier's base structure to its term-model [[J]]-structure (definitional, as the [[J]]-structure interprets Sum.inl symbols by the base reduct). Lets realize_mapLanguage transfer realizations of base-language formulas.