The local EM truth lemma, layer 2: readiness + the staged truth lemma

The truth-lemma endpoints of the EMContext re-base, ported from EMTermModel.lean:1030–1379 (Steps 4D-7 and 4D-9) onto the countable local stack. Three parts.

Generic readiness (section TruthReadiness, over any [Λ.Structure M]): the ⋁/⋀- completeness mixin LocalEMContext.OmegaComplete with its easy directions (eventualDeepTruth_iSup_of_exists, eventualDeepTruth_iInf_forall), the decidedness predicate LocalEMContext.Decided, and the recursive readiness predicate LocalEMContext.TLReady. Ported from EMTermModel.lean:1041–1102 with the skolemColim letI plumbing dropped (the structure is the ambient instance, as throughout LocalEMContext.lean).

Staged readiness over localColim s₀ (section StagedReadiness, over an arbitrary [(localColim s₀).Structure M]): the support-uniform staged readiness LocalEMContext.TLReadyStage (EMTermModel.lean:1117–1127), the deForm-closure mixin LocalEMContext.DeFormClosedForColim — rephrased over the colimit-level family ΓlocalColim rather than the staged Γ* of EMContext.DeFormClosedForGammaStar (EMTermModel.lean:1308–1319); staged members reach it via toLocalColimFormula_mem_ΓlocalColim — and the family-readiness endpoints TLReady_mapLang_of_Γlocal_succ / TLReadyStage_of_Γlocal_succ (EMTermModel.lean:1322–1377). Unlike the EM stack, where the mixin stays an open obligation, here it has a concrete two-line discharger deFormClosedForColim_of_ΓEMlocal_subset (via locDeForm_mem_ΓEMlocal), a pure parameterized lemma: it takes ΓEMlocal s₀ ⊆ ctx.Γ as a hypothesis; the application against exists_localEMContext (whose context has ctx.Γ = ΓEMlocal s₀) happens downstream in the Conditional-touching extraction layer, not here.

The staged truth lemma (section StagedTruthLemma, over a source model [s₀.Lang.Structure M] with letI := localColimStructure s₀ in the statements, as in locSkWitness_universal): LocalEMContext.truthLemmaStage, the port of EMContext.truthLemmaStage (EMTermModel.lean:1129–1291), plus the stage-k lift corollary truthLemmaStage_of_mem. Two deliberate statement-shape divergences from the EM original:

• Membership threading. The local Skolem witness locSkWitnessTerm exists only for family members (it is keyed by a Γlocal-membership proof, where the EM skWitnessTerm takes an arbitrary formula), so the induction carries hmem : ⟨n, ψ⟩ ∈ Γlocal s₀ (k + 1) and each case derives its subformulas' memberships via bfSubformulas_subset_Γlocal_succ before applying the IH. In the all case the memberships split: hmem itself (the .all member) feeds the witness API (locSkWitnessTerm, locSkWitness_universal), while the body membership for the IH comes from bfSubformulas_subset_Γlocal_succ hmem.
• Successor-stage placement. Subformula closure of Γlocal holds only at successor stages (bfSubformulas_subset_Γlocal_succ; the stage-0 seed is raw), so the readiness and truth-lemma endpoints are stated for ψ : (Llocal s₀ (k + 1)).BoundedFormulaω Empty n with membership in Γlocal s₀ (k + 1), mapped via LlocalInclusion s₀ (k + 1). The lift corollary truthLemmaStage_of_mem restores the stage-agnostic form for original stage-k members via liftGamma_mem_Γlocal_succ + the cocone coherence LlocalInclusion_comp_LlocalHom.

The completeness input remains an assumed mixin (hc), but in the honest restricted form OmegaCompleteForColim (= OmegaCompleteOn at ΓlocalColim s₀): the induction only ever consumes ⋁/⋀-completeness at colimit images of family members, whose memberships it threads — while an arbitrary tail-indiscernible sequence can have drifting witnesses for countable disjunctions outside the family, so the global OmegaComplete (kept, with the adapter OmegaComplete.toOmegaCompleteOn) is strictly stronger than any extraction needs to deliver. Producing the restricted witness ("ΓlocalColim-restricted witness homogeneity") is later work, as is the final connection to TailTemplateRealizable. This is a pure file (imports LocalEMTruth, hence the pure local stack only) — no EM-stack or Conditional/ reach.

Generic truth-lemma readiness

The ⋁/⋀-completeness mixin, decidedness, and the recursive readiness predicate, generic over any [Λ.Structure M]. Ported from EMTermModel.lean:1041–1102.

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

⋁/⋀-completeness of a LocalEMContext's eventual deep truth: the genuinely non-formal residual for the countable connectives — a uniform iSup-witness and a uniform iInf-cutoff. Since atTop on ℕ is not countably complete, neither follows from tail indiscernibility + decidedness; they are the infinitary analogue of the consistency-property C3/C4 rules for ⋁/⋀, packaged as a separate Prop mixin (not core LocalEMContext fields, so the quotient/congruence/atom API is untouched). The truth lemma takes hc : ctx.OmegaComplete; producing such a context is later work. Local analogue of EMContext.OmegaComplete.

• iSup_complete {m : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty m) (ts : Fin m → (Λ.withConstants J).Term Empty) (S : Finset J) : eventualDeepTruth Λ J ctx (BoundedFormulaω.iSup φs) ts S → ∃ (i : ℕ), eventualDeepTruth Λ J ctx (φs i) ts S

  Eventual deep truth of ⋁φs provides a single component witness.

• iInf_complete {m : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty m) (ts : Fin m → (Λ.withConstants J).Term Empty) (S : Finset J) : (∀ (i : ℕ), eventualDeepTruth Λ J ctx (φs i) ts S) → eventualDeepTruth Λ J ctx (BoundedFormulaω.iInf φs) ts S

  Eventual deep truth of all components provides eventual deep truth of ⋀φs.

structure FirstOrder.Language.LocalEMContext.OmegaCompleteOn (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (Γ' : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)) : Prop

Γ-restricted, support-covered ⋁/⋀-completeness: like OmegaComplete, but the uniform iSup-witness and uniform iInf-cutoff are demanded only at disjunctions/conjunctions that are members of the family Γ', and only at argument tuples whose skeleton support is covered by the ambient support (hcov). This is the honest form of the obligation: the staged truth-lemma induction only ever consumes completeness at colimit images of family members (their memberships are threaded through the induction) and always under a support-covering proof (hsub), while an arbitrary tail-indiscernible sequence can have drifting witnesses for countable disjunctions outside the family — so the global OmegaComplete is strictly stronger than what any extraction argument needs to deliver. The covering makes the clauses deForm- normalizable (eventualDeepTruth_iff_eventual_locDeForm), hence reducible to the source-side LocalEMOmegaHomogeneous below.

• iSup_complete {m : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty m) : ⟨m, BoundedFormulaω.iSup φs⟩ ∈ Γ' → ∀ (ts : Fin m → (Λ.withConstants J).Term Empty) (S : Finset J), (∀ (i : Fin m), Λ.locJSupport J (ts i) ⊆ S) → eventualDeepTruth Λ J ctx (BoundedFormulaω.iSup φs) ts S → ∃ (i : ℕ), eventualDeepTruth Λ J ctx (φs i) ts S

  Eventual deep truth of a family disjunction ⋁φs ∈ Γ', over a covered support, provides a single component witness.

• iInf_complete {m : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty m) : ⟨m, BoundedFormulaω.iInf φs⟩ ∈ Γ' → ∀ (ts : Fin m → (Λ.withConstants J).Term Empty) (S : Finset J), (∀ (i : Fin m), Λ.locJSupport J (ts i) ⊆ S) → (∀ (i : ℕ), eventualDeepTruth Λ J ctx (φs i) ts S) → eventualDeepTruth Λ J ctx (BoundedFormulaω.iInf φs) ts S

  Eventual deep truth of all components of a family conjunction ⋀φs ∈ Γ', over a covered support, provides eventual deep truth of the conjunction.

theorem FirstOrder.Language.LocalEMContext.OmegaComplete.toOmegaCompleteOn (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] {ctx : Λ.LocalEMContext J} (hc : OmegaComplete Λ J ctx) (Γ' : Set ((n : ℕ) × Λ.BoundedFormulaω Empty n)) : OmegaCompleteOn Λ J ctx Γ'

Compatibility adapter: global completeness restricts to any family and any covering — existing OmegaComplete producers serve every OmegaCompleteOn consumer by dropping the membership and the covering.

theorem FirstOrder.Language.LocalEMContext.eventualDeepTruth_iSup_of_exists (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {m : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty m) (ts : Fin m → (Λ.withConstants J).Term Empty) (S : Finset J) (h : ∃ (i : ℕ), eventualDeepTruth Λ J ctx (φs i) ts S) : eventualDeepTruth Λ J ctx (BoundedFormulaω.iSup φs) ts S

The easy iSup direction: a single component's eventual deep truth gives the disjunction's.

theorem FirstOrder.Language.LocalEMContext.eventualDeepTruth_iInf_forall (Λ : Language) (J : Type) [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {m : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty m) (ts : Fin m → (Λ.withConstants J).Term Empty) (S : Finset J) (h : eventualDeepTruth Λ J ctx (BoundedFormulaω.iInf φs) ts S) (i : ℕ) : eventualDeepTruth Λ J ctx (φs i) ts S

The easy iInf direction: the conjunction's eventual deep truth gives every component's.

deForm normal forms

Over a covered support, eventual deep truth is eventual truth of the de-substituted source formula on consecutive ctx.a-tuples — and de-substitution commutes syntactically with the countable connectives. Together these turn the support-covered Ω-clauses into pure statements about the source sequence (LocalEMOmegaHomogeneous below).

theorem FirstOrder.Language.LocalEMContext.eventualDeepTruth_iff_eventual_locDeForm (Λ : 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) : eventualDeepTruth Λ J ctx φ ts S ↔ ∀ᶠ (d : ℕ) in Filter.atTop, (Λ.locDeForm J S φ ts hsub).Realize Empty.elim fun (k : Fin S.card) => ctx.a (d + ↑k)

deForm normal form for eventual deep truth: over a covered support, the eventual deep truth of φ on ts/S is the eventual truth of the de-substituted locDeForm S φ ts on the consecutive deep tuples k ↦ ctx.a (d + k). Pointwise realize_locDeForm.

theorem FirstOrder.Language.locDeForm_iSup (Λ : Language) (J : Type) [LinearOrder J] {n : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty n) (ts : Fin n → (Λ.withConstants J).Term Empty) {S : Finset J} (hsub : ∀ (i : Fin n), Λ.locJSupport J (ts i) ⊆ S) : Λ.locDeForm J S (BoundedFormulaω.iSup φs) ts hsub = BoundedFormulaω.iSup fun (i : ℕ) => Λ.locDeForm J S (φs i) ts hsub

De-substitution commutes with ⋁ (the openBounds → subst → relabel template is structural).

theorem FirstOrder.Language.locDeForm_iInf (Λ : Language) (J : Type) [LinearOrder J] {n : ℕ} (φs : ℕ → Λ.BoundedFormulaω Empty n) (ts : Fin n → (Λ.withConstants J).Term Empty) {S : Finset J} (hsub : ∀ (i : Fin n), Λ.locJSupport J (ts i) ⊆ S) : Λ.locDeForm J S (BoundedFormulaω.iInf φs) ts hsub = BoundedFormulaω.iInf fun (i : ℕ) => Λ.locDeForm J S (φs i) ts hsub

De-substitution commutes with ⋀.

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

Decidedness of a formula's eventual deep truth (the named output of eventualDeepTruth_decided): either it holds eventually, or it fails eventually. Local analogue of EMContext.Decided, with the ambient [Λ.Structure M] in place of the skolemColim letI.

Equations

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

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

Truth-lemma readiness of a formula on ts/S: the closure data the truth-lemma induction consumes — decidedness at every imp-antecedent (for eventualDeepTruth_imp_iff), recursively down the connectives. The all φ case requires the body φ to be ready at every one-point extension Fin.snoc ts u (the carrier's ∀x ranges over all term-classes mkClass u via Quotient.ind), so the all case recurses on the structural subformula φ — no Skolem-witness recursion is needed here. Discharged from the family deForm-closure via eventualDeepTruth_decided. Local analogue of EMContext.TLReady.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.Language.LocalEMContext.TLReady Λ J ctx FirstOrder.Language.BoundedFormulaω.falsum x✝¹ x✝ = True
• FirstOrder.Language.LocalEMContext.TLReady Λ J ctx (FirstOrder.Language.BoundedFormulaω.equal t₁ t₂) x✝¹ x✝ = True
• FirstOrder.Language.LocalEMContext.TLReady Λ J ctx (FirstOrder.Language.BoundedFormulaω.rel R ts) x✝¹ x✝ = True
• FirstOrder.Language.LocalEMContext.TLReady Λ J ctx (FirstOrder.Language.BoundedFormulaω.iSup φs) x✝¹ x✝ = ∀ (i : ℕ), FirstOrder.Language.LocalEMContext.TLReady Λ J ctx (φs i) x✝¹ x✝
• FirstOrder.Language.LocalEMContext.TLReady Λ J ctx (FirstOrder.Language.BoundedFormulaω.iInf φs) x✝¹ x✝ = ∀ (i : ℕ), FirstOrder.Language.LocalEMContext.TLReady Λ J ctx (φs i) x✝¹ x✝

Staged readiness over localColim s₀

The support-uniform staged readiness, the colimit-level deForm-closure mixin with its ΓEMlocal discharger, and the family-readiness endpoints. Over an arbitrary [(localColim s₀).Structure M] — no source-model semantics enters until the truth lemma itself.

def FirstOrder.Language.LocalEMContext.TLReadyStage (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (ctx : (localColim s₀).LocalEMContext J) (k : ℕ) {n : ℕ} (ψ : (Llocal s₀ k).BoundedFormulaω Empty n) (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (S : Finset J) : Prop

Staged truth-lemma readiness (support-uniform): the colimit TLReady of the staged formula's image under LlocalInclusion k holds at every enlarged support T ⊇ S. The uniformity is what the all case needs — it reads the body's readiness at S ∪ locJSupport u (for the Skolem witness, whose own support is ⊆ S). Monotone in S by construction; the successor-stage family discharges it uniformly (TLReadyStage_of_Γlocal_succ). Local analogue of EMContext.TLReadyStage.

Equations

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

@[reducible, inline]

abbrev FirstOrder.Language.LocalEMContext.OmegaCompleteForColim (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (ctx : (localColim s₀).LocalEMContext J) : Prop

The colimit-family completeness obligation — the exact ⋁/⋀-completeness the staged truth lemma consumes: OmegaCompleteOn at the colimit family ΓlocalColim s₀. This, not the global OmegaComplete, is the final residual shape the witness-homogeneous extraction has to deliver ("ΓlocalColim-restricted witness homogeneity").

Equations

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

structure FirstOrder.Language.LocalEMOmegaHomogeneous (s₀ : LocalStage) {M : Type} [(localColim s₀).Structure M] (a : ℕ → M) : Prop

Source-side Ω-homogeneity of a sequence — the deForm normal form of the support-covered completeness obligation, freed of the term model entirely: no J, no supports, no quotient, no LocalEMContext. For each family disjunction/conjunction (member of ΓlocalColim s₀) and each canonical de-substitution tuple g (through which every J/ts/S instance factors, via locDeTermFin), the uniform witness/cutoff exchange holds for the eventual truth of the de-substituted components on consecutive a-tuples. This is a pure statement about the sequence a in the source model — the shape the remaining combinatorial extraction has to homogenize.

• iSup_homogeneous {m : ℕ} (φs : ℕ → (localColim s₀).BoundedFormulaω Empty m) : ⟨m, BoundedFormulaω.iSup φs⟩ ∈ ΓlocalColim s₀ → ∀ {p : ℕ} (g : Fin m → (localColim s₀).Term (Fin p)), (∀ᶠ (d : ℕ) in Filter.atTop, ∃ (i : ℕ), ((localColim s₀).canonDeForm (φs i) g).Realize Empty.elim fun (k : Fin p) => a (d + ↑k)) → ∃ (i : ℕ), ∀ᶠ (d : ℕ) in Filter.atTop, ((localColim s₀).canonDeForm (φs i) g).Realize Empty.elim fun (k : Fin p) => a (d + ↑k)

  Uniform iSup-witness: if, eventually in depth, some de-substituted component of a family disjunction holds on the consecutive tuple, then a single component eventually holds.

• iInf_homogeneous {m : ℕ} (φs : ℕ → (localColim s₀).BoundedFormulaω Empty m) : ⟨m, BoundedFormulaω.iInf φs⟩ ∈ ΓlocalColim s₀ → ∀ {p : ℕ} (g : Fin m → (localColim s₀).Term (Fin p)), (∀ (i : ℕ), ∀ᶠ (d : ℕ) in Filter.atTop, ((localColim s₀).canonDeForm (φs i) g).Realize Empty.elim fun (k : Fin p) => a (d + ↑k)) → ∀ᶠ (d : ℕ) in Filter.atTop, ∀ (i : ℕ), ((localColim s₀).canonDeForm (φs i) g).Realize Empty.elim fun (k : Fin p) => a (d + ↑k)

  Uniform iInf-cutoff: if every de-substituted component of a family conjunction eventually holds on the consecutive tuple, then eventually all components hold simultaneously.

theorem FirstOrder.Language.LocalEMContext.omegaCompleteForColim_of_omegaHomogeneous (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (ctx : (localColim s₀).LocalEMContext J) (h : LocalEMOmegaHomogeneous s₀ ctx.a) : OmegaCompleteForColim s₀ J ctx

The reduction theorem: source-side Ω-homogeneity of the context's sequence delivers the support-covered colimit-family completeness — the term-model side of the obligation dissolves. Each Ω-clause converts pointwise through realize_locDeForm (with locDeForm definitionally the canonical deForm at the locDeTermFin tuple, so the homogeneity fields apply at g := locDeTermFin ∘ ts), and realize_iSup/realize_iInf split the connective on the deep side. After this, the remaining extraction target is LocalEMOmegaHomogeneous alone.

structure FirstOrder.Language.LocalEMContext.DeFormClosedForColim (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (ctx : (localColim s₀).LocalEMContext J) : Prop

deForm-membership closure (construction-data mixin, the seam between family readiness and the extracted family): every colimit-family member's de-substituted formula — support-uniformly, i.e. over every argument tuple ts, covering support T, and covering proof hcov — lies in ctx.Γ. Rephrased over the colimit-level ΓlocalColim rather than the staged Γ* of EMContext.DeFormClosedForGammaStar; staged members reach it via toLocalColimFormula_mem_ΓlocalColim. Discharged by deFormClosedForColim_of_ΓEMlocal_subset.

• deForm_mem {n : ℕ} {φ : (localColim s₀).BoundedFormulaω Empty n} : ⟨n, φ⟩ ∈ ΓlocalColim s₀ → ∀ (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (T : Finset J) (hcov : ∀ (i : Fin n), (localColim s₀).locJSupport J (ts i) ⊆ T), ⟨T.card, (localColim s₀).locDeForm J T φ ts hcov⟩ ∈ ctx.Γ

  Each colimit-family member's deForm, over any covering support and arguments, is in Γ.

theorem FirstOrder.Language.LocalEMContext.deFormClosedForColim_of_ΓEMlocal_subset (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (ctx : (localColim s₀).LocalEMContext J) (hΓ : ΓEMlocal s₀ ⊆ ctx.Γ) : DeFormClosedForColim s₀ J ctx

The deForm-closure mixin, discharged (pure parameterized form): any context whose family contains ΓEMlocal s₀ is deForm-closed for the colimit family, via locDeForm_mem_ΓEMlocal. In contrast to the EM stack, where DeFormClosedForGammaStar stays an open obligation, the local family was built with the canonical deForm closure inside. The hypothesis hΓ is discharged downstream against exists_localEMContext (whose context has ctx.Γ = ΓEMlocal s₀) — in the extraction layer, not here, keeping this file pure.

theorem FirstOrder.Language.LocalEMContext.TLReady_mapLang_of_Γlocal_succ (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (ctx : (localColim s₀).LocalEMContext J) {k : ℕ} (hclosed : DeFormClosedForColim s₀ J ctx) {n : ℕ} (ψ : (Llocal s₀ (k + 1)).BoundedFormulaω Empty n) : ⟨n, ψ⟩ ∈ Γlocal s₀ (k + 1) → ∀ (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (T : Finset J), (∀ (i : Fin n), (localColim s₀).locJSupport J (ts i) ⊆ T) → TLReady (localColim s₀) J ctx (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ (k + 1)) ψ) ts T

Readiness (un-quantified support form): from the deForm-closure mixin, every successor-stage family formula ψ has TLReady at every covering support T. The core induction; TLReadyStage_of_Γlocal_succ wraps it over T ⊇ S. Stated at stage k + 1 because subformula closure holds only at successor stages (bfSubformulas_subset_Γlocal_succ); the membership recursion descends through it, and the imp-antecedent decidedness obligations are discharged by eventualDeepTruth_decided fed by the mixin. Local analogue of EMContext.TLReady_mapLang_of_GammaStar.

theorem FirstOrder.Language.LocalEMContext.TLReadyStage_of_Γlocal_succ (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (ctx : (localColim s₀).LocalEMContext J) {k : ℕ} (hclosed : DeFormClosedForColim s₀ J ctx) {n : ℕ} (ψ : (Llocal s₀ (k + 1)).BoundedFormulaω Empty n) (hψ : ⟨n, ψ⟩ ∈ Γlocal s₀ (k + 1)) (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (S : Finset J) (hcov : ∀ (i : Fin n), (localColim s₀).locJSupport J (ts i) ⊆ S) : TLReadyStage s₀ J ctx (k + 1) ψ ts S

The successor-stage family supplies support-uniform TLReadyStage (this chunk's readiness endpoint, modulo the deForm-closure mixin hclosed): every Γlocal s₀ (k + 1) formula is truthLemmaStage-ready. Wraps TLReady_mapLang_of_Γlocal_succ over the enlarged supports T ⊇ S (each still covers ts). Local analogue of EMContext.TLReadyStage_of_GammaStar.

theorem FirstOrder.Language.mapLanguage_LlocalInclusion_lift (s₀ : LocalStage) {k n : ℕ} (ψ : (Llocal s₀ k).BoundedFormulaω Empty n) : BoundedFormulaω.mapLanguage (LlocalInclusion s₀ (k + 1)) (BoundedFormulaω.mapLanguage (LlocalHom s₀ k) ψ) = BoundedFormulaω.mapLanguage (LlocalInclusion s₀ k) ψ

Formula-level cocone coherence for the truth lemma's lift: mapping a stage-k formula one stage up (along LlocalHom) and then into the colimit is the direct colimit image. The formula component of toLocalColimFormula_step, in the un-packaged form the stage-k lift corollary rewrites with.

theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_eq_iSup {L₁ L₂ : Language} {g : L₁ →ᴸ L₂} {α : Type} {m : ℕ} {ψ : L₁.BoundedFormulaω α m} {φs : ℕ → L₂.BoundedFormulaω α m} (h : mapLanguage g ψ = iSup φs) : ∃ (ψs : ℕ → L₁.BoundedFormulaω α m), ψ = iSup ψs ∧ ∀ (i : ℕ), φs i = mapLanguage g (ψs i)

Constructor inversion for mapLanguage at ⋁: language maps preserve constructor heads, so a ⋁-image comes from a ⋁-preimage, componentwise. Feeds the colimit component-membership lemmas below.

theorem FirstOrder.Language.BoundedFormulaω.mapLanguage_eq_iInf {L₁ L₂ : Language} {g : L₁ →ᴸ L₂} {α : Type} {m : ℕ} {ψ : L₁.BoundedFormulaω α m} {φs : ℕ → L₂.BoundedFormulaω α m} (h : mapLanguage g ψ = iInf φs) : ∃ (ψs : ℕ → L₁.BoundedFormulaω α m), ψ = iInf ψs ∧ ∀ (i : ℕ), φs i = mapLanguage g (ψs i)

Constructor inversion for mapLanguage at ⋀.

theorem FirstOrder.Language.iSup_component_mem_ΓlocalColim (s₀ : LocalStage) {m : ℕ} {φs : ℕ → (localColim s₀).BoundedFormulaω Empty m} (h : ⟨m, BoundedFormulaω.iSup φs⟩ ∈ ΓlocalColim s₀) (i : ℕ) : ⟨m, φs i⟩ ∈ ΓlocalColim s₀

Components of colimit-family disjunctions stay in the colimit family: a ⋁ in ΓlocalColim is the colimit image of a staged ⋁ (constructor inversion), whose components reach the successor family by lift + subformula closure, hence the colimit family by the cocone coherence. The membership plumbing that feeds the full-indiscernibility Ω-restoration at the colimit family.

theorem FirstOrder.Language.iInf_component_mem_ΓlocalColim (s₀ : LocalStage) {m : ℕ} {φs : ℕ → (localColim s₀).BoundedFormulaω Empty m} (h : ⟨m, BoundedFormulaω.iInf φs⟩ ∈ ΓlocalColim s₀) (i : ℕ) : ⟨m, φs i⟩ ∈ ΓlocalColim s₀

Components of colimit-family conjunctions stay in the colimit family.

theorem FirstOrder.Language.LocalEMContext.TLReadyStage_of_Γlocal (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (ctx : (localColim s₀).LocalEMContext J) {k : ℕ} (hclosed : DeFormClosedForColim s₀ J ctx) {n : ℕ} (ψ : (Llocal s₀ k).BoundedFormulaω Empty n) (hψ : ⟨n, ψ⟩ ∈ Γlocal s₀ k) (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (S : Finset J) (hcov : ∀ (i : Fin n), (localColim s₀).locJSupport J (ts i) ⊆ S) : TLReadyStage s₀ J ctx k ψ ts S

Stage-agnostic readiness: every stage-k family member — including the raw seed stage 0, where subformula closure is not available — is TLReadyStage-ready, by lifting one stage (along LlocalHom, via liftGamma_mem_Γlocal_succ) and rewriting the colimit image back down with the cocone coherence mapLanguage_LlocalInclusion_lift.

The staged truth lemma (over a source model)

The load-bearing endpoint: over a source model [s₀.Lang.Structure M] with letI := localColimStructure s₀ in the statements (the locSkWitness_universal pattern — the all case consumes the Skolem transport, which holds only for the concrete colimit structure). exists_localEMContext uses the same letI pattern but lives downstream in LocalEMExtraction and is not used or imported here.

theorem FirstOrder.Language.LocalEMContext.truthLemmaStage_of_skolemUniversal (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (hsk : LocalSkolemUniversalForColim s₀) (ctx : (localColim s₀).LocalEMContext J) : OmegaCompleteForColim s₀ J ctx → ∀ (k : ℕ) {n : ℕ} (ψ : (Llocal s₀ (k + 1)).BoundedFormulaω Empty n), ⟨n, ψ⟩ ∈ Γlocal s₀ (k + 1) → ∀ (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (S : Finset J), (∀ (i : Fin n), (localColim s₀).locJSupport J (ts i) ⊆ S) → TLReadyStage s₀ J ctx (k + 1) ψ ts S → (((BoundedFormulaω.mapLanguage ((localColim s₀).lhomWithConstants J) (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ (k + 1)) ψ)).Realize Empty.elim fun (i : Fin n) => mkClass (localColim s₀) J ctx (ts i)) ↔ eventualDeepTruth (localColim s₀) J ctx (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ (k + 1)) ψ) ts S)

The staged local truth lemma, generic core: over ANY localColim structure on the source satisfying the Skolem-universality mixin LocalSkolemUniversalForColim — the schema term model supplies a non-canonical instance. For a successor-stage family formula ψ ∈ Γlocal s₀ (k + 1), realizing its colimit image in the local EM term model on term-classes is equivalent to its eventual deep truth. Structural induction on ψ threading the family membership (each case derives its subformulas' memberships via bfSubformulas_subset_Γlocal_succ): atoms/connectives via the layer-1 kernel (mapLanguage distributes definitionally), iSup/iInf via hc : ctx.OmegaComplete, and the all case via the Skolem-witness transport — the witness locSkWitnessTerm is keyed by the .all membership hmem itself, has support ⊆ S, and support-uniform readiness supplies the body's readiness at every enlarged support. The Skolem step is discharged by the mixin (locSkWitness_universal_of_mixin); the canonical wrapper below restores the original inline form. Local analogue of EMContext.truthLemmaStage.

The completeness input is the restricted OmegaCompleteForColim: the iSup/iInf cases consume it only at the colimit images of family members, whose memberships the induction threads (global OmegaComplete users go through OmegaComplete.toOmegaCompleteOn).

theorem FirstOrder.Language.LocalEMContext.truthLemmaStage_of_mem_of_skolemUniversal (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [(localColim s₀).Structure M] (hsk : LocalSkolemUniversalForColim s₀) (ctx : (localColim s₀).LocalEMContext J) : OmegaCompleteForColim s₀ J ctx → ∀ (k : ℕ) {n : ℕ} (ψ : (Llocal s₀ k).BoundedFormulaω Empty n), ⟨n, ψ⟩ ∈ Γlocal s₀ k → ∀ (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (S : Finset J), (∀ (i : Fin n), (localColim s₀).locJSupport J (ts i) ⊆ S) → TLReadyStage s₀ J ctx k ψ ts S → (((BoundedFormulaω.mapLanguage ((localColim s₀).lhomWithConstants J) (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ k) ψ)).Realize Empty.elim fun (i : Fin n) => mkClass (localColim s₀) J ctx (ts i)) ↔ eventualDeepTruth (localColim s₀) J ctx (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ k) ψ) ts S)

Stage-agnostic lift corollary, generic core: the staged truth lemma for an original stage-k family member, at any stage including the raw seed stage 0, over any mixin-satisfying structure. Lifts the member one stage (along LlocalHom, via liftGamma_mem_Γlocal_succ) where subformula closure is available, then rewrites the colimit image back down with the cocone coherence mapLanguage_LlocalInclusion_lift.

Canonical wrappers (the original theorem names, over localColimStructure)

theorem FirstOrder.Language.LocalEMContext.truthLemmaStage (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [s₀.Lang.Structure M] [Nonempty M] (ctx : (localColim s₀).LocalEMContext J) : OmegaCompleteForColim s₀ J ctx → ∀ (k : ℕ) {n : ℕ} (ψ : (Llocal s₀ (k + 1)).BoundedFormulaω Empty n), ⟨n, ψ⟩ ∈ Γlocal s₀ (k + 1) → ∀ (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (S : Finset J), (∀ (i : Fin n), (localColim s₀).locJSupport J (ts i) ⊆ S) → TLReadyStage s₀ J ctx (k + 1) ψ ts S → (((BoundedFormulaω.mapLanguage ((localColim s₀).lhomWithConstants J) (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ (k + 1)) ψ)).Realize Empty.elim fun (i : Fin n) => mkClass (localColim s₀) J ctx (ts i)) ↔ eventualDeepTruth (localColim s₀) J ctx (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ (k + 1)) ψ) ts S)

The staged local truth lemma over the canonical localColimStructure — the original endpoint, now a wrapper supplying localSkolemUniversalForColim_canonical to the generic core.

theorem FirstOrder.Language.LocalEMContext.truthLemmaStage_of_mem (s₀ : LocalStage) (J : Type) [LinearOrder J] {M : Type} [s₀.Lang.Structure M] [Nonempty M] (ctx : (localColim s₀).LocalEMContext J) : OmegaCompleteForColim s₀ J ctx → ∀ (k : ℕ) {n : ℕ} (ψ : (Llocal s₀ k).BoundedFormulaω Empty n), ⟨n, ψ⟩ ∈ Γlocal s₀ k → ∀ (ts : Fin n → ((localColim s₀).withConstants J).Term Empty) (S : Finset J), (∀ (i : Fin n), (localColim s₀).locJSupport J (ts i) ⊆ S) → TLReadyStage s₀ J ctx k ψ ts S → (((BoundedFormulaω.mapLanguage ((localColim s₀).lhomWithConstants J) (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ k) ψ)).Realize Empty.elim fun (i : Fin n) => mkClass (localColim s₀) J ctx (ts i)) ↔ eventualDeepTruth (localColim s₀) J ctx (BoundedFormulaω.mapLanguage (LlocalInclusion s₀ k) ψ) ts S)

Stage-agnostic lift corollary over the canonical localColimStructure — the original endpoint, now a wrapper around the generic core.