The countable local colimit language L_Γ (localColim) and its cocone

The hinge of the L_Γ pivot. LocalTower.lean builds the mutually recursive tower Llocal s₀ k / Γlocal s₀ k and proves every stage countable; this file assembles the tower into an actual colimit language and shows countability survives to the colimit — the object the EM term model must be re-based over (the full skolemColim is uncountable, so its atom diagram cannot fit inside the countable family the tail extraction delivers).

Mirrors the skolemColim layer of SkolemColimit.lean exactly (same DirectedColim quotient, same Quot.lift colimit structure, same definitional stage coherence), plus what skolemColim cannot have: countability of the colimit symbol types and of the colimit image ΓlocalColim of the staged families.

• localColim s₀ — the colimit language L_Γ = colim_k (Llocal s₀ k).
• LlocalInclusion s₀ k — the cocone Llocal s₀ k →ᴸ localColim s₀, with symbol-level cocone-compatibility (LlocalInclusion_onFunction_step/_onRelation_step).
• localColim_fun_countable / localColim_rel_countable — the payoff: the colimit language is countable (via DirectedColim.countable, a sequential colimit of countable types).
• localStageStructure / localColimStructure / LlocalInclusion_isExpansionOn / realize_map_LlocalInclusion — the semantic-transport API on a fixed s₀.Lang-model M.
• toLocalColimFormula / ΓlocalColim / ΓlocalColim_countable — the (countable) colimit image of the staged families, the family the truth lemma will consume.
• Formula-level cocone coherence for the EM rebase: LlocalInclusion_comp_LlocalHom, toLocalColimFormula_step, toLocalColimFormula_lift_mem_ΓlocalColim, and localSkolemWitnessFormula_mem_ΓlocalColim (the skolemNeed witness body of every family universal lands in ΓlocalColim).

Next chunks (not here): the local atom/deForm seed and its countability, then the EMContext re-base over localColim.

theorem FirstOrder.Language.DirectedColim.countable {F : ℕ → Type} {φ : (k : ℕ) → F k → F (k + 1)} (h : ∀ (k : ℕ), Countable (F k)) : Countable (DirectedColim F φ)

A sequential colimit of countable types is countable: the colimit is a quotient of the countable total space Σ k, F k. (Generic companion to DirectedColim; the reason the local colimit stays countable while skolemColim does not.)

theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_mapLanguage {L₁ L₂ L₃ : Language} (g : L₁ →ᴸ L₂) (h : L₂ →ᴸ L₃) {α : Type u_1} {n : ℕ} (φ : L₁.BoundedFormulaω α n) : mapLanguage h (mapLanguage g φ) = mapLanguage (h.comp g) φ

mapLanguage composes: transporting along g then h is transporting along h.comp g. (A Mathlib-gap-style generic lemma; belongs in Lomega1omega/Operations.lean eventually — localized here, where the cocone coherence needs it, to keep the default build path untouched.)

theorem FirstOrder.Language.Llocal_functions_countable (s₀ : LocalStage) (k m : ℕ) : Countable ((Llocal s₀ k).Functions m)

Per-arity function-symbol countability at each stage (the fibre of the stagewise all-arity certificate Llocal_fun_countable).

theorem FirstOrder.Language.Llocal_relations_countable (s₀ : LocalStage) (k m : ℕ) : Countable ((Llocal s₀ k).Relations m)

Per-arity relation-symbol countability at each stage.

The colimit language L_Γ and the stage cocone

def FirstOrder.Language.localColim (s₀ : LocalStage) : Language

The local colimit language L_Γ = colim_k (Llocal s₀ k): function/relation symbols at each arity are the sequential colimits of the staged symbol types along LlocalHom. Every L_Γ-symbol lives at a finite stage; in particular every family formula's existential acquires its local Skolem function at the next stage, so L_Γ is Skolem-complete for the family.

Equations

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

def FirstOrder.Language.LlocalInclusion (s₀ : LocalStage) (k : ℕ) : Llocal s₀ k →ᴸ localColim s₀

The cocone: the inclusion of stage k into the local colimit language L_Γ. On symbols it is the colimit inclusion DirectedColim.incl k.

Equations

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

theorem FirstOrder.Language.LlocalInclusion_onFunction_step (s₀ : LocalStage) {k m : ℕ} (f : (Llocal s₀ k).Functions m) : (LlocalInclusion s₀ (k + 1)).onFunction ((LlocalHom s₀ k).onFunction f) = (LlocalInclusion s₀ k).onFunction f

Cocone compatibility on function symbols: pushing a stage-k symbol one stage up and then into the colimit is the same as including it directly.

theorem FirstOrder.Language.LlocalInclusion_onRelation_step (s₀ : LocalStage) {k m : ℕ} (r : (Llocal s₀ k).Relations m) : (LlocalInclusion s₀ (k + 1)).onRelation ((LlocalHom s₀ k).onRelation r) = (LlocalInclusion s₀ k).onRelation r

Cocone compatibility on relation symbols.

theorem FirstOrder.Language.LlocalInclusion_comp_LlocalHom (s₀ : LocalStage) (k : ℕ) : (LlocalInclusion s₀ (k + 1)).comp (LlocalHom s₀ k) = LlocalInclusion s₀ k

Cocone compatibility as an LHom equation: including stage k via stage k+1 is the direct inclusion. The formula-level coherence (toLocalColimFormula_step) is this plus mapLanguage composition.

Countability of the colimit language — the payoff of the pivot

theorem FirstOrder.Language.localColim_functions_countable (s₀ : LocalStage) (m : ℕ) : Countable ((localColim s₀).Functions m)

Per-arity: the colimit function symbols are countable.

theorem FirstOrder.Language.localColim_relations_countable (s₀ : LocalStage) (m : ℕ) : Countable ((localColim s₀).Relations m)

Per-arity: the colimit relation symbols are countable.

theorem FirstOrder.Language.localColim_fun_countable (s₀ : LocalStage) : Countable ((n : ℕ) × (localColim s₀).Functions n)

The local colimit language has countably many function symbols — in contrast to skolemColim, whose function-symbol type has the cardinality of the continuum.

theorem FirstOrder.Language.localColim_rel_countable (s₀ : LocalStage) : Countable ((n : ℕ) × (localColim s₀).Relations n)

The local colimit language has countably many relation symbols.

Stage structures on a fixed model and the colimit structure

@[implicit_reducible]

noncomputable def FirstOrder.Language.localStageStructure (s₀ : LocalStage) {M : Type} [s₀.Lang.Structure M] [Nonempty M] (k : ℕ) : (Llocal s₀ k).Structure M

The stage-k structure on a fixed s₀.Lang-model M: stage 0 is M's own structure, and each successor stage adds the Hilbert-choice interpretation of the new local Skolem symbols (localSkolemStructure) on top of the previous stage, via the sum structure.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.localStageStructure s₀ 0 = inst✝¹

theorem FirstOrder.Language.localStageStructure_funMap_succ (s₀ : LocalStage) {M : Type} [s₀.Lang.Structure M] [Nonempty M] {k m : ℕ} (f : (Llocal s₀ k).Functions m) (x : Fin m → M) : Structure.funMap ((LlocalHom s₀ k).onFunction f) x = Structure.funMap f x

Stage coherence (functions): a stage-k symbol pushed to stage k+1 interprets the same way. This is the cocone-compatibility witnessing the colimit interpretation is well-defined.

theorem FirstOrder.Language.localStageStructure_relMap_succ (s₀ : LocalStage) {M : Type} [s₀.Lang.Structure M] [Nonempty M] {k m : ℕ} (r : (Llocal s₀ k).Relations m) (x : Fin m → M) : Structure.RelMap ((LlocalHom s₀ k).onRelation r) x = Structure.RelMap r x

Stage coherence (relations).

@[implicit_reducible]

noncomputable def FirstOrder.Language.localColimStructure (s₀ : LocalStage) {M : Type} [s₀.Lang.Structure M] [Nonempty M] : (localColim s₀).Structure M

The colimit structure: an L_Γ-symbol is interpreted through any stage representative, well-defined by the (definitional) stage coherence above.

Equations

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

theorem FirstOrder.Language.LlocalInclusion_isExpansionOn (s₀ : LocalStage) {M : Type} [s₀.Lang.Structure M] [Nonempty M] (k : ℕ) : (LlocalInclusion s₀ k).IsExpansionOn M

The stage inclusion is an expansion: the colimit structure restricts to the stage structure along LlocalInclusion (the colimit funMap/RelMap on an included symbol computes — by rfl — to the stage interpretation).

theorem FirstOrder.Language.realize_map_LlocalInclusion (s₀ : LocalStage) {M : Type} [s₀.Lang.Structure M] [Nonempty M] (k : ℕ) {n : ℕ} (φ : (Llocal s₀ k).BoundedFormulaω Empty n) (v : Empty → M) (xs : Fin n → M) : (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ k) φ).Realize v xs ↔ φ.Realize v xs

Semantic preservation by stage inclusion: transporting a stage-k formula into L_Γ along LlocalInclusion preserves its realization in M. Immediate from realize_mapLanguage and the expansion property above.

The colimit image of the staged families

def FirstOrder.Language.toLocalColimFormula (s₀ : LocalStage) (k : ℕ) (p : (n : ℕ) × (Llocal s₀ k).BoundedFormulaω Empty n) : (n : ℕ) × (localColim s₀).BoundedFormulaω Empty n

Transport an arity-tagged stage-k formula into the local colimit language along the cocone inclusion.

Equations

• FirstOrder.Language.toLocalColimFormula s₀ k p = ⟨p.fst, FirstOrder.Language.BoundedFormulaω.mapLanguage (FirstOrder.Language.LlocalInclusion s₀ k) p.snd⟩

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

The colimit family Γ_Γ ⊆ L_Γ-formulas: the union over all stages of the colimit images of the staged families Γlocal s₀ k. This is the family over which the re-based EM term model's truth lemma will run.

Equations

• FirstOrder.Language.ΓlocalColim s₀ = ⋃ (k : ℕ), FirstOrder.Language.toLocalColimFormula s₀ k '' FirstOrder.Language.Γlocal s₀ k

theorem FirstOrder.Language.toLocalColimFormula_mem_ΓlocalColim (s₀ : LocalStage) {k : ℕ} {p : (n : ℕ) × (Llocal s₀ k).BoundedFormulaω Empty n} (hp : p ∈ Γlocal s₀ k) : toLocalColimFormula s₀ k p ∈ ΓlocalColim s₀

Stage membership transports into the colimit family.

theorem FirstOrder.Language.ΓlocalColim_countable (s₀ : LocalStage) : (ΓlocalColim s₀).Countable

The colimit family is countable: a countable union of images of the (stagewise countable) families. Together with localColim_fun_countable/_rel_countable, this says the local Skolem construction really does produce a countable language and family in the colimit — the exact size interface the tail extraction (MorleyHanfExtractionTail) can serve.

Formula-level cocone coherence

The wrappers the EM rebase will consume, so its proofs never touch raw mapLanguage equalities.

theorem FirstOrder.Language.toLocalColimFormula_step (s₀ : LocalStage) (k : ℕ) (p : (n : ℕ) × (Llocal s₀ k).BoundedFormulaω Empty n) : toLocalColimFormula s₀ (k + 1) ⟨p.fst, BoundedFormulaω.mapLanguage (LlocalHom s₀ k) p.snd⟩ = toLocalColimFormula s₀ k p

Formula-level cocone coherence: a stage-k formula lifted one stage (along LlocalHom) and then included into the colimit is the same colimit formula as including it directly.

theorem FirstOrder.Language.toLocalColimFormula_lift_mem_ΓlocalColim (s₀ : LocalStage) {k : ℕ} {p : (n : ℕ) × (Llocal s₀ k).BoundedFormulaω Empty n} (hp : p ∈ Γlocal s₀ k) : toLocalColimFormula s₀ (k + 1) ⟨p.fst, BoundedFormulaω.mapLanguage (LlocalHom s₀ k) p.snd⟩ ∈ ΓlocalColim s₀

Lifted membership: the stage-(k+1) lift of a stage-k family member has its colimit image in ΓlocalColim — and by toLocalColimFormula_step that image coincides with the direct stage-k image, so the two membership routes agree.

theorem FirstOrder.Language.localSkolemWitnessFormula_mem_ΓlocalColim (s₀ : LocalStage) {k n : ℕ} {ψ : (Llocal s₀ k).BoundedFormulaω Empty (n + 1)} (h : ⟨n, ψ.all⟩ ∈ Γlocal s₀ k) : toLocalColimFormula s₀ (k + 1) ⟨n, localSkolemWitnessFormula (skolemNeedSymbol h)⟩ ∈ ΓlocalColim s₀

Witness-body membership in the colimit family: for every universal member ∀ψ of a stage family, the local Skolem witness body of ¬ψ (available at the next stage thanks to skolemNeed) has its colimit image in ΓlocalColim — the closure fact the rebased truth lemma's all-case readiness will cite.