Documentation

LeanPool.InfinitaryLogic.Methods.LocalEMTruthLemma

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:

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.

source
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.

Instances For

    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).

    source
    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
    Instances For

      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.

      source
      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.
      Instances For
        source
        @[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.
        Instances For
          source
          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.

          Instances For
            source
            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.

            source
            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.

            Instances For
              source
              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.

              source
              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.

              source
              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.

              source
              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.

              source
              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.

              source
              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).

              source
              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.