The countable local atom/deForm family ΓEMlocal

The size bottleneck of the EM re-base, resolved. The EM term model's EMContext needs a tail-indiscernible family Γ containing every de-substituted atom (atom_mem/rel_mem) and the deForms of the truth-lemma family (DeFormClosedForGammaStar); the tail extraction (MorleyHanfExtractionTail) delivers indiscernibility only over a countable Γ. Over skolemColim L the atom diagram is uncountable and the context cannot be instantiated; this file builds the countable replacement over localColim s₀.

The factoring insight: a de-substituted atom/deForm over a support S : Finset J depends on its Λ[[J]]-terms only through their de-substitutions to Fin S.card-variable Λ-terms. So the family of ALL such formulas — over EVERY linear order J, every support, every closed term — factors through the canonical (J-free) seeds indexed by Σ m, Λ.Term (Fin m)-data, which are countable whenever Λ is. Concretely, the local locDeEqAtom/locDeRelAtom/locDeForm are defined as canonical seeds applied to locDeTermFin-images, so factoring is definitional and membership in the canonical seeds is by construction.

Contents:

• Canonical seeds over any Λ : Language.{0,0}: canonEqAtom(s), canonRelAtom(s), canonDeForm(s) + countability (canonEqAtoms_countable etc.) from countable symbol types.
• The J-side de-substitution pipeline over any Λ (mirroring the skolemColim-specific chain in EMTermModel.lean; the generic pieces deepRank/Term.varFinset_relabel live in the shared LocalEMSupport.lean): locJConstOf, locJSupport, locDeTermPos, locDeTermFin, and the local atoms/deForm locDeEqAtom/locDeRelAtom/locDeForm with membership in the canonical seeds.
• The assembled family ΓEMlocal s₀ = ΓlocalColim ∪ eq-atoms ∪ rel-atoms ∪ deForms(ΓlocalColim) over localColim s₀, with ΓEMlocal_countable, the membership interface the future local EMContext instantiation will discharge (locDeEqAtom_mem_ΓEMlocal = atom_mem, locDeRelAtom_mem_ΓEMlocal = rel_mem, locDeForm_mem_ΓEMlocal = the deForm closure), and the enumeration exists_ΓEMlocalEnum in the exact shape the tail extraction consumes.

The GENERIC semantic (realize) bridges live in LocalEMContext.lean; the old skolemColim-specific ones remain in EMTermModel.lean. This file is deliberately purely syntactic.

Canonical (J-free) seeds over a countable language

def FirstOrder.Language.canonEqAtom (Λ : Language) {m : ℕ} (t u : Λ.Term (Fin m)) : Λ.BoundedFormulaω Empty m

The canonical equality atom of two Fin m-variable terms: the arity-m formula t = u with the variables rebound. Every de-substituted equality atom (over any J, any support) is definitionally of this shape.

Equations

• Λ.canonEqAtom t u = FirstOrder.Language.BoundedFormulaω.equal (FirstOrder.Language.Term.relabel Sum.inr t) (FirstOrder.Language.Term.relabel Sum.inr u)

def FirstOrder.Language.canonEqAtoms (Λ : Language) : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)

The canonical equality-atom seed: all canonical equality atoms, over all arities.

Equations

• Λ.canonEqAtoms = Set.range fun (p : (m : ℕ) × Λ.Term (Fin m) × Λ.Term (Fin m)) => ⟨p.fst, Λ.canonEqAtom p.snd.1 p.snd.2⟩

theorem FirstOrder.Language.canonEqAtoms_countable (Λ : Language) (hf : Countable ((n : ℕ) × Λ.Functions n)) : Λ.canonEqAtoms.Countable

The canonical equality-atom seed is countable when Λ's function symbols are: it is the range of a map from Σ m, (Λ.Term (Fin m))², countable by Mathlib's term encoding.

def FirstOrder.Language.canonRelAtom (Λ : Language) {m l : ℕ} (R : Λ.Relations l) (ts : Fin l → Λ.Term (Fin m)) : Λ.BoundedFormulaω Empty m

The canonical relation atom: a relation symbol applied to rebound Fin m-variable terms.

Equations

• Λ.canonRelAtom R ts = FirstOrder.Language.BoundedFormulaω.rel R fun (i : Fin l) => FirstOrder.Language.Term.relabel Sum.inr (ts i)

def FirstOrder.Language.canonRelAtoms (Λ : Language) : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)

The canonical relation-atom seed: all canonical relation atoms, over all arities and all relation symbols.

Equations

• Λ.canonRelAtoms = Set.range fun (q : (m : ℕ) × (l : ℕ) × Λ.Relations l × (Fin l → Λ.Term (Fin m))) => ⟨q.fst, Λ.canonRelAtom q.snd.snd.1 q.snd.snd.2⟩

theorem FirstOrder.Language.canonRelAtoms_countable (Λ : Language) (hf : Countable ((n : ℕ) × Λ.Functions n)) (hr : Countable ((n : ℕ) × Λ.Relations n)) : Λ.canonRelAtoms.Countable

The canonical relation-atom seed is countable when Λ's symbol types are.

def FirstOrder.Language.canonDeForm (Λ : Language) {n : ℕ} (φ : Λ.BoundedFormulaω Empty n) {p : ℕ} (g : Fin n → Λ.Term (Fin p)) : Λ.BoundedFormulaω Empty p

The canonical deForm of a formula φ (arity n) along a tuple of Fin p-variable terms: open the bound variables, substitute the terms, rebind the p positions — the openBounds → subst → relabel template of EMTermModel.deForm, with the J-dependence already factored out.

Equations

• Λ.canonDeForm φ g = FirstOrder.Language.BoundedFormulaω.relabel Sum.inr (FirstOrder.Language.BoundedFormulaω.subst φ.openBounds g)

def FirstOrder.Language.canonDeForms (Λ : Language) (Γc : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)) : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)

The canonical deForm closure of a base family Γc: all canonical deForms of its members, over all target arities and term tuples.

Equations

• Λ.canonDeForms Γc = ⋃ q ∈ Γc, Set.range fun (r : (p : ℕ) × (Fin q.fst → Λ.Term (Fin p))) => ⟨r.fst, Λ.canonDeForm q.snd r.snd⟩

theorem FirstOrder.Language.canonDeForms_countable (Λ : Language) {Γc : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)} (hΓc : Γc.Countable) (hf : Countable ((n : ℕ) × Λ.Functions n)) : (Λ.canonDeForms Γc).Countable

The canonical deForm closure of a countable family is countable.

theorem FirstOrder.Language.canonDeForm_mem_canonDeForms (Λ : Language) {Γc : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)} {n : ℕ} {φ : Λ.BoundedFormulaω Empty n} (hφ : ⟨n, φ⟩ ∈ Γc) {p : ℕ} (g : Fin n → Λ.Term (Fin p)) : ⟨p, Λ.canonDeForm φ g⟩ ∈ Λ.canonDeForms Γc

Membership constructor for the canonical deForm closure.

The J-side de-substitution pipeline

Mirrors the skolemColim-specific chain of EMTermModel.lean over an arbitrary Λ (the generic pieces deepRank, deepRank_lt_card, Term.varFinset_relabel live in the shared LocalEMSupport.lean). The loc prefix disambiguates from the skolemColim versions.

def FirstOrder.Language.locJConstOf (Λ : Language) (J : Type) {n : ℕ} : (Λ.withConstants J).Functions n → Finset J

The J-constant carried by a function symbol of Λ[[J]]: only an arity-0 symbol from the constantsOn J summand is a skeleton constant.

Equations

• Λ.locJConstOf J (Sum.inr j) = {j}
• Λ.locJConstOf J x✝ = ∅

def FirstOrder.Language.locJSupport (Λ : Language) (J : Type) [LinearOrder J] {α : Type} : (Λ.withConstants J).Term α → Finset J

The finite set of J-constants (skeleton constants) mentioned in a Λ[[J]]-term.

Equations

• Λ.locJSupport J (FirstOrder.Language.var a) = ∅
• Λ.locJSupport J (FirstOrder.Language.func f ts) = (Finset.univ.biUnion fun (i : Fin l) => Λ.locJSupport J (ts i)) ∪ Λ.locJConstOf J f

theorem FirstOrder.Language.locConstantsToVars_varFinset_subset (Λ : Language) (J : Type) [LinearOrder J] (t : (Λ.withConstants J).Term Empty) : t.constantsToVars.varFinset ⊆ Finset.image Sum.inl (Λ.locJSupport J t)

The de-substituted term constantsToVars t uses only the variables Sum.inl j for j a skeleton constant of t.

def FirstOrder.Language.locDeTermPos (Λ : Language) (J : Type) [LinearOrder J] (S : Finset J) (t : (Λ.withConstants J).Term Empty) : Λ.Term ℕ

The de-substituted term at ordered support positions: each skeleton constant c_j becomes the ℕ-variable deepRank S j.

Equations

• Λ.locDeTermPos J S t = FirstOrder.Language.Term.relabel (Sum.elim (fun (j : J) => FirstOrder.Language.deepRank J S j) Empty.elim) t.constantsToVars

theorem FirstOrder.Language.locDeTermPos_varFinset_subset (Λ : Language) (J : Type) [LinearOrder J] {S : Finset J} {t : (Λ.withConstants J).Term Empty} (hsub : Λ.locJSupport J t ⊆ S) : (Λ.locDeTermPos J S t).varFinset ⊆ Finset.range S.card

The ordered-position term uses only variables < S.card once S covers the term's skeleton constants.

def FirstOrder.Language.locDeTermFin (Λ : Language) (J : Type) [LinearOrder J] (S : Finset J) (t : (Λ.withConstants J).Term Empty) (hsub : Λ.locJSupport J t ⊆ S) : Λ.Term (Fin S.card)

The de-substituted term at Fin S.card positions: locDeTermPos with its variables packaged as genuine Fin S.card indices. The finite-variable term through which every J-dependent atom/deForm factors.

Equations

• Λ.locDeTermFin J S t hsub = (Λ.locDeTermPos J S t).restrictVar fun (x : ↥(Λ.locDeTermPos J S t).varFinset) => ⟨↑x, ⋯⟩

Local atoms and deForm — canonical seeds applied to de-substituted terms

def FirstOrder.Language.locDeEqAtom (Λ : Language) (J : Type) [LinearOrder J] (S : Finset J) (t u : (Λ.withConstants J).Term Empty) (ht : Λ.locJSupport J t ⊆ S) (hu : Λ.locJSupport J u ⊆ S) : Λ.BoundedFormulaω Empty S.card

The local de-substituted equality atom: definitionally a canonical equality atom, so its membership in canonEqAtoms is by construction.

Equations

• Λ.locDeEqAtom J S t u ht hu = Λ.canonEqAtom (Λ.locDeTermFin J S t ht) (Λ.locDeTermFin J S u hu)

theorem FirstOrder.Language.locDeEqAtom_mem_canonEqAtoms (Λ : Language) (J : Type) [LinearOrder J] (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⟩ ∈ Λ.canonEqAtoms

Factoring, equality case: every local equality atom lies in the canonical (J-free) seed.

def FirstOrder.Language.locDeRelAtom (Λ : Language) (J : Type) [LinearOrder J] (S : Finset J) {l : ℕ} (R : Λ.Relations l) (ts : Fin l → (Λ.withConstants J).Term Empty) (ht : ∀ (i : Fin l), Λ.locJSupport J (ts i) ⊆ S) : Λ.BoundedFormulaω Empty S.card

The local de-substituted relation atom: definitionally a canonical relation atom.

Equations

• Λ.locDeRelAtom J S R ts ht = Λ.canonRelAtom R fun (i : Fin l) => Λ.locDeTermFin J S (ts i) ⋯

theorem FirstOrder.Language.locDeRelAtom_mem_canonRelAtoms (Λ : Language) (J : Type) [LinearOrder J] (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⟩ ∈ Λ.canonRelAtoms

Factoring, relation case: every local relation atom lies in the canonical seed.

def FirstOrder.Language.locDeForm (Λ : Language) (J : Type) [LinearOrder J] (S : Finset J) {n : ℕ} (φ : Λ.BoundedFormulaω Empty n) (ts : Fin n → (Λ.withConstants J).Term Empty) (hsub : ∀ (i : Fin n), Λ.locJSupport J (ts i) ⊆ S) : Λ.BoundedFormulaω Empty S.card

The local general de-substituted formula: definitionally a canonical deForm of φ.

Equations

• Λ.locDeForm J S φ ts hsub = Λ.canonDeForm φ fun (i : Fin n) => Λ.locDeTermFin J S (ts i) ⋯

theorem FirstOrder.Language.locDeForm_mem_canonDeForms (Λ : Language) (J : Type) [LinearOrder J] {Γc : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)} (S : Finset J) {n : ℕ} {φ : Λ.BoundedFormulaω Empty n} (hφ : ⟨n, φ⟩ ∈ Γc) (ts : Fin n → (Λ.withConstants J).Term Empty) (hsub : ∀ (i : Fin n), Λ.locJSupport J (ts i) ⊆ S) : ⟨S.card, Λ.locDeForm J S φ ts hsub⟩ ∈ Λ.canonDeForms Γc

Factoring, deForm case: the local deForm of any member of a base family lies in that family's canonical deForm closure.

The assembled family ΓEMlocal over the local colimit

def FirstOrder.Language.ΓEMlocal (s₀ : LocalStage) : Set ((n : ℕ) × (localColim s₀).BoundedFormulaω Empty n)

The extracted-family candidate: the colimit family together with the full canonical atom seeds and the canonical deForm closure of the colimit family — everything the local EMContext's hind/atom_mem/rel_mem/deForm-closure obligations will quantify over.

Equations

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

theorem FirstOrder.Language.ΓEMlocal_countable (s₀ : LocalStage) : (ΓEMlocal s₀).Countable

The size bottleneck, resolved: ΓEMlocal is countable — the family the tail extraction (MorleyHanfExtractionTail) can actually serve, in contrast to the uncountable skolemColim atom diagram.

theorem FirstOrder.Language.ΓlocalColim_subset_ΓEMlocal (s₀ : LocalStage) : ΓlocalColim s₀ ⊆ ΓEMlocal s₀

The colimit family sits inside ΓEMlocal.

theorem FirstOrder.Language.locDeEqAtom_mem_ΓEMlocal (J : Type) [LinearOrder J] (s₀ : LocalStage) (S : Finset J) (t u : ((localColim s₀).withConstants J).Term Empty) (ht : (localColim s₀).locJSupport J t ⊆ S) (hu : (localColim s₀).locJSupport J u ⊆ S) : ⟨S.card, (localColim s₀).locDeEqAtom J S t u ht hu⟩ ∈ ΓEMlocal s₀

atom_mem discharger: every local equality atom — over every J, support, and pair of closed terms — lies in ΓEMlocal.

theorem FirstOrder.Language.locDeRelAtom_mem_ΓEMlocal (J : Type) [LinearOrder J] (s₀ : LocalStage) (S : Finset J) {l : ℕ} (R : (localColim s₀).Relations l) (ts : Fin l → ((localColim s₀).withConstants J).Term Empty) (ht : ∀ (i : Fin l), (localColim s₀).locJSupport J (ts i) ⊆ S) : ⟨S.card, (localColim s₀).locDeRelAtom J S R ts ht⟩ ∈ ΓEMlocal s₀

rel_mem discharger: every local relation atom lies in ΓEMlocal.

theorem FirstOrder.Language.locDeForm_mem_ΓEMlocal (J : Type) [LinearOrder J] (s₀ : LocalStage) (S : Finset J) {n : ℕ} {φ : (localColim s₀).BoundedFormulaω Empty n} (hφ : ⟨n, φ⟩ ∈ ΓlocalColim s₀) (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (hsub : ∀ (i : Fin n), (localColim s₀).locJSupport J (ts i) ⊆ S) : ⟨S.card, (localColim s₀).locDeForm J S φ ts hsub⟩ ∈ ΓEMlocal s₀

deForm-closure discharger: the local deForm of every colimit-family member lies in ΓEMlocal — the content of the future local DeFormClosedForGammaStar.

theorem FirstOrder.Language.ΓEMlocal_nonempty (s₀ : LocalStage) : (ΓEMlocal s₀).Nonempty

ΓEMlocal is nonempty (the arity-1 atom x = x is a canonical equality atom).

theorem FirstOrder.Language.exists_ΓEMlocalEnum (s₀ : LocalStage) : ∃ (e : ℕ → (n : ℕ) × (localColim s₀).BoundedFormulaω Empty n), ΓEMlocal s₀ = Set.range e

An enumeration of ΓEMlocal as a sequence — the exact shape the tail extraction (morleyHanfExtractionTail_holds, whose extraction yields tail-indiscernibility on Set.range) consumes.