Layer 7b checkpoint 5a: the schema term-model substrate

The completed schema theory Tσ = schemaCompletionTheory (schemaEnumeration s₀) hM is complete on the schema universe, iSup-witnessed, and finite-character consistent — but NOT a maximal ConsistencyPropertyEq (deliberately: the pivot escaped the extension-field blocker). So its term model's equality quotient cannot come from a syntactic C6-closure of Tσ. Instead, per the design decision, equality on closed (localColim s₀)[[ℕ]] terms is defined directly in the locDeEqAtom vocabulary the completion controls, and every quotient law (reflexivity, symmetry, transitivity, congruence, relation well-definedness) is proved by the same source-semantic contradiction: if the wrong sign were in Tσ, finite_consistent yields a source-model body realizing an impossible equality situation in M.

The file delivers checkpoint 5a in full: the canonical-support equality relation SchemaTermEq and the shared body-extraction engine exists_body_of_subset; the exported semantic bridges realize_schemaEqSentence_iff/realize_schemaRelSentence_iff (via the σ-generalization locDeTermFin_realize_constInterp_nat); the equivalence/congruence laws; and the quotient model — SchemaTermCarrier with its (localColim s₀)[[ℕ]]-structure, the atomic API (schemaTerm_funMap_mk/schemaTerm_realize_eq_mk/schemaTerm_relMap_mk_iff), and the canonical sequence schemaSeq (the classes of the d-constants). No iSup, all, or truth lemma here — that is checkpoint 5b.

def FirstOrder.Language.schemaSupport {s₀ : LocalStage} (t u : ((localColim s₀).withConstants ℕ).Term Empty) : Finset ℕ

The canonical finite support of an equality between two closed schema terms.

Equations

• FirstOrder.Language.schemaSupport t u = (FirstOrder.Language.localColim s₀).locJSupport ℕ t ∪ (FirstOrder.Language.localColim s₀).locJSupport ℕ u

def FirstOrder.Language.schemaEqSentence {s₀ : LocalStage} (t u : ((localColim s₀).withConstants ℕ).Term Empty) : (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω

The lifted templateSentence of the de-substituted equality atom locDeEqAtom at the canonical support — the schema-universe sentence that encodes "t = u".

Equations

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

theorem FirstOrder.Language.schemaEqSentence_mem_universe {s₀ : LocalStage} (t u : ((localColim s₀).withConstants ℕ).Term Empty) : ⟨schemaEqSentence t u, ⋯⟩ ∈ schemaFSentenceUniverse s₀

schemaEqSentence t u is a schema-universe member (its de-substituted atom is in ΓEMlocal).

def FirstOrder.Language.SchemaTermEq {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (t u : ((localColim s₀).withConstants ℕ).Term Empty) : Prop

Canonical-support schema equality on closed (localColim s₀)[[ℕ]] terms: t ≈ u iff the completed theory contains the encoded equality sentence.

Equations

• FirstOrder.Language.SchemaTermEq hM t u = (FirstOrder.Language.schemaEqSentence t u ∈ FirstOrder.Language.schemaCompletionTheory (FirstOrder.Language.schemaEnumeration s₀) hM)

theorem FirstOrder.Language.exists_body_of_subset {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (F : Finset (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω) (hF : ∀ τ ∈ F, τ ∈ schemaCompletionTheory (schemaEnumeration s₀) hM) : ∃ (σ : ℕ → M) (h : ℕ → M), ∀ τ ∈ F, realizeWith σ h τ Empty.elim Fin.elim0

The shared body-extraction engine. A finite fragment of Tσ is MarkerHenkinConsistent, so it has a body: a source interpretation (σ, h) realizing every member. Every equality law derives its contradiction from this.

theorem FirstOrder.Language.locDeEqAtom_self_realize {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] {S : Finset ℕ} (t : ((localColim s₀).withConstants ℕ).Term Empty) (ht : (localColim s₀).locJSupport ℕ t ⊆ S) (w : Fin S.card → M) : ((localColim s₀).locDeEqAtom ℕ S t t ht ht).Realize Empty.elim w

The de-substituted equality atom of a term with itself realizes to True (reflexivity of the underlying =), on any valuation.

theorem FirstOrder.Language.locDeTermFin_realize_constInterp_nat {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] (σ : ℕ → M) {S : Finset ℕ} (t : ((localColim s₀).withConstants ℕ).Term Empty) (hsub : (localColim s₀).locJSupport ℕ t ⊆ S) : Term.realize (fun (i : Fin S.card) => σ ((S.orderEmbOfFin ⋯) i)) ((localColim s₀).locDeTermFin ℕ S t hsub) = Term.realize Empty.elim t

The σ-generalization of locDeTermFin_realize (specialized to J := ℕ): the de-substituted term, realized on the tuple of σ-values of its support, equals the closed term realized under the σ-constant interpretation. Unlike locDeTermFin_realize, the interpretation σ is arbitrary (not a deep a-tuple) — exactly what the body from exists_body_of_subset supplies. Adapts the locDeTermFin_realize_superset pattern (restrictVar + constantsToVars + realize_eq_of_eq_on_varFinset + orderEmbOfFin_deepRank).

theorem FirstOrder.Language.schemaTermEq_refl {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (t : ((localColim s₀).withConstants ℕ).Term Empty) : SchemaTermEq hM t t

Reflexivity. t ≈ t: the theory decides schemaEqSentence t t; the negative sign is impossible because any source body would have to realize ¬(t = t).

theorem FirstOrder.Language.realize_schemaEqSentence_iff {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] (σ h : ℕ → M) (t u : ((localColim s₀).withConstants ℕ).Term Empty) : realizeWith σ h (schemaEqSentence t u) Empty.elim Fin.elim0 ↔ Term.realize Empty.elim t = Term.realize Empty.elim u

The exported equality bridge. Under a body interpretation (σ, h), schemaEqSentence t u is realized iff t and u have the same σ-value — the semantically meaningful form every equality law consumes.

theorem FirstOrder.Language.schemaTermEq_symm {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {t u : ((localColim s₀).withConstants ℕ).Term Empty} (h : SchemaTermEq hM t u) : SchemaTermEq hM u t

Symmetry. t ≈ u → u ≈ t: a body realizing t = u and ¬(u = t) contradicts Eq.symm.

theorem FirstOrder.Language.schemaTermEq_trans {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {t u v : ((localColim s₀).withConstants ℕ).Term Empty} (h1 : SchemaTermEq hM t u) (h2 : SchemaTermEq hM u v) : SchemaTermEq hM t v

Transitivity. t ≈ u → u ≈ v → t ≈ v: a body realizing t = u, u = v, ¬(t = v) contradicts Eq.trans.

theorem FirstOrder.Language.schemaTermEq_func {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {n : ℕ} (f : ((localColim s₀).withConstants ℕ).Functions n) (ts us : Fin n → ((localColim s₀).withConstants ℕ).Term Empty) (h : ∀ (i : Fin n), SchemaTermEq hM (ts i) (us i)) : SchemaTermEq hM (func f ts) (func f us)

Function congruence. If ts i ≈ us i for every argument, then f ts ≈ f us: a body realizing all the argument equalities and ¬(f ts = f us) contradicts the function interpretation respecting equal arguments. This makes the quotient's funMap well-defined.

The relation interface (schemaRelSentence + well-definedness)

def FirstOrder.Language.schemaRelSupport {s₀ : LocalStage} {l : ℕ} (ts : Fin l → ((localColim s₀).withConstants ℕ).Term Empty) : Finset ℕ

The canonical finite support of a relation atom over a tuple of closed schema terms.

Equations

• FirstOrder.Language.schemaRelSupport ts = Finset.univ.biUnion fun (i : Fin l) => (FirstOrder.Language.localColim s₀).locJSupport ℕ (ts i)

theorem FirstOrder.Language.locJSupport_subset_schemaRelSupport {s₀ : LocalStage} {l : ℕ} (ts : Fin l → ((localColim s₀).withConstants ℕ).Term Empty) (i : Fin l) : (localColim s₀).locJSupport ℕ (ts i) ⊆ schemaRelSupport ts

def FirstOrder.Language.schemaRelSentence {s₀ : LocalStage} {l : ℕ} (R : (localColim s₀).Relations l) (ts : Fin l → ((localColim s₀).withConstants ℕ).Term Empty) : (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω

The lifted templateSentence of the de-substituted relation atom locDeRelAtom at the canonical support — the schema-universe sentence that encodes "R ts".

Equations

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

theorem FirstOrder.Language.schemaRelSentence_mem_universe {s₀ : LocalStage} {l : ℕ} (R : (localColim s₀).Relations l) (ts : Fin l → ((localColim s₀).withConstants ℕ).Term Empty) : ⟨schemaRelSentence R ts, ⋯⟩ ∈ schemaFSentenceUniverse s₀

schemaRelSentence R ts is a schema-universe member.

theorem FirstOrder.Language.realize_schemaRelSentence_iff {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] (σ h : ℕ → M) {l : ℕ} (R : (localColim s₀).Relations l) (ts : Fin l → ((localColim s₀).withConstants ℕ).Term Empty) : realizeWith σ h (schemaRelSentence R ts) Empty.elim Fin.elim0 ↔ Structure.RelMap R fun (i : Fin l) => Term.realize Empty.elim (ts i)

The exported relation bridge. Under a body interpretation (σ, h), schemaRelSentence R ts is realized iff R holds in M on the σ-values of the terms.

def FirstOrder.Language.SchemaTermRel {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {l : ℕ} (R : (localColim s₀).Relations l) (ts : Fin l → ((localColim s₀).withConstants ℕ).Term Empty) : Prop

Canonical-support schema relation membership on tuples of closed schema terms.

Equations

• FirstOrder.Language.SchemaTermRel hM R ts = (FirstOrder.Language.schemaRelSentence R ts ∈ FirstOrder.Language.schemaCompletionTheory (FirstOrder.Language.schemaEnumeration s₀) hM)

theorem FirstOrder.Language.schemaTermRel_congr {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {l : ℕ} (R : (localColim s₀).Relations l) {ts us : Fin l → ((localColim s₀).withConstants ℕ).Term Empty} (h : ∀ (i : Fin l), SchemaTermEq hM (ts i) (us i)) (hR : SchemaTermRel hM R ts) : SchemaTermRel hM R us

Relation well-definedness. Argument-wise SchemaTermEq preserves SchemaTermRel: a body realizing R ts, all argument equalities, and ¬(R us) contradicts M's RelMap respecting equal arguments. This makes the quotient's RelMap well-defined.

The quotient term model

def FirstOrder.Language.schemaTermSetoid {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) : Setoid (((localColim s₀).withConstants ℕ).Term Empty)

The setoid on closed schema terms induced by the completed theory.

Equations

• FirstOrder.Language.schemaTermSetoid hM = { r := FirstOrder.Language.SchemaTermEq hM, iseqv := ⋯ }

@[reducible, inline]

abbrev FirstOrder.Language.SchemaTermCarrier {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) : Type

The schema term-model carrier: closed (localColim s₀)[[ℕ]] terms quotiented by the completed theory's equality. An abbrev, so Quotient lemmas and dot-notation apply transparently (the FSentence precedent).

Equations

• FirstOrder.Language.SchemaTermCarrier hM = Quotient (FirstOrder.Language.schemaTermSetoid hM)

@[reducible, inline]

abbrev FirstOrder.Language.SchemaTermCarrier.mk {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (t : ((localColim s₀).withConstants ℕ).Term Empty) : SchemaTermCarrier hM

The class of a closed schema term.

Equations

• FirstOrder.Language.SchemaTermCarrier.mk hM t = ⟦t⟧

instance FirstOrder.Language.instNonemptySchemaTermCarrier {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) : Nonempty (SchemaTermCarrier hM)

The carrier is inhabited (class of the first sequence constant d₀).

theorem FirstOrder.Language.SchemaTermCarrier.mk_eq_mk_iff {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {t u : ((localColim s₀).withConstants ℕ).Term Empty} : mk hM t = mk hM u ↔ SchemaTermEq hM t u

Two terms have the same class iff the completed theory contains their equality sentence.

theorem FirstOrder.Language.SchemaTermCarrier.mk_out_eq {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (t : ((localColim s₀).withConstants ℕ).Term Empty) : SchemaTermEq hM (Quotient.out (mk hM t)) t

The representative of a class is equivalent to the term that formed it.

@[reducible]

noncomputable def FirstOrder.Language.schemaTermStructure {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) : ((localColim s₀).withConstants ℕ).Structure (SchemaTermCarrier hM)

The (localColim s₀)[[ℕ]]-structure on the carrier: funMap by term formation on Quotient.out representatives; RelMap (the constant layer adds no relations) by the completed theory's relation membership on representatives. Well-definedness on classes is exposed by the atomic API below (via schemaTermEq_func/schemaTermRel_congr), not baked into the definition.

Equations

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

theorem FirstOrder.Language.schemaTerm_funMap_mk {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {n : ℕ} (f : ((localColim s₀).withConstants ℕ).Functions n) (ts : Fin n → ((localColim s₀).withConstants ℕ).Term Empty) : (Structure.funMap f fun (i : Fin n) => SchemaTermCarrier.mk hM (ts i)) = SchemaTermCarrier.mk hM (func f ts)

Atomic API, function symbols: funMap computes on classes — applying an interpreted symbol to classes gives the class of the function term (well-definedness via schemaTermEq_func).

theorem FirstOrder.Language.schemaTerm_realize_eq_mk {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (t : ((localColim s₀).withConstants ℕ).Term Empty) : Term.realize Empty.elim t = SchemaTermCarrier.mk hM t

Atomic API, terms: every closed term realizes in the term model to its own class.

theorem FirstOrder.Language.schemaTerm_relMap_mk_iff {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {l : ℕ} (R : (localColim s₀).Relations l) (ts : Fin l → ((localColim s₀).withConstants ℕ).Term Empty) : (Structure.RelMap (Sum.inl R) fun (i : Fin l) => SchemaTermCarrier.mk hM (ts i)) ↔ SchemaTermRel hM R ts

Atomic API, relations: a base relation holds in the term model on classes iff the completed theory contains the relation sentence (well-definedness via schemaTermRel_congr).

noncomputable def FirstOrder.Language.schemaSeq {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (n : ℕ) : SchemaTermCarrier hM

The canonical schema sequence in the term model: the classes of the sequence constants d₀, d₁, …. This is the sequence the witnessed template (TailTemplateOmegaWitnessed) will be established for.

Equations

• FirstOrder.Language.schemaSeq hM n = FirstOrder.Language.SchemaTermCarrier.mk hM (FirstOrder.Language.henkinConst n)

The general schema-formula interface and semantic sign transport (5b-3 substrate)

The restricted truth lemma treats equality/relation sentences as special cases of ONE formula-application encoding: schemaFormulaSentence φ ts, the lifted template of the general de-substituted formula locDeForm at the canonical support schemaRelSupport ts. Its source-semantics bridge realize_schemaFormulaSentence_iff is the semantic engine of the truth lemma. The sign-transport lemmas then move theory membership across ANY semantic equivalence of universe sentences (support changes, canonical deForms, normalization to the atomic API) by one body extraction — never by re-running quotient inductions: if the two sentences carried opposite signs, exists_body_of_subset would realize both the source and the negated target under one interpretation pair, contradicting the equivalence.

def FirstOrder.Language.schemaFormulaSentence {s₀ : LocalStage} {n : ℕ} (φ : (localColim s₀).BoundedFormulaω Empty n) (ts : Fin n → ((localColim s₀).withConstants ℕ).Term Empty) : (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω

The lifted templateSentence of the general de-substituted formula locDeForm at the canonical support — the schema-universe sentence that encodes "φ holds on the closed terms ts". schemaEqSentence/schemaRelSentence are the atomic special cases of this shape.

Equations

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

theorem FirstOrder.Language.schemaFormulaSentence_mem_universe {s₀ : LocalStage} {n : ℕ} {φ : (localColim s₀).BoundedFormulaω Empty n} (hφ : ⟨n, φ⟩ ∈ ΓlocalColim s₀) (ts : Fin n → ((localColim s₀).withConstants ℕ).Term Empty) : ⟨schemaFormulaSentence φ ts, ⋯⟩ ∈ schemaFSentenceUniverse s₀

schemaFormulaSentence φ ts of a colimit-family member is a schema-universe member (its de-substituted formula is in the canonDeForms component of ΓEMlocal).

theorem FirstOrder.Language.realize_schemaFormulaSentence_iff {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] (σ h : ℕ → M) {n : ℕ} (φ : (localColim s₀).BoundedFormulaω Empty n) (ts : Fin n → ((localColim s₀).withConstants ℕ).Term Empty) : realizeWith σ h (schemaFormulaSentence φ ts) Empty.elim Fin.elim0 ↔ φ.Realize Empty.elim fun (i : Fin n) => Term.realize Empty.elim (ts i)

The exported formula bridge — the truth lemma's semantic engine. Under a body interpretation (σ, h), schemaFormulaSentence φ ts is realized iff φ holds in M on the σ-values of the closed terms. Generalizes realize_schemaEqSentence_iff/ realize_schemaRelSentence_iff to arbitrary formulas via the same σ-generalized term bridge.

theorem FirstOrder.Language.schemaLift_mem_of_semantic_imp {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {m : ℕ} {ψ : (localColim s₀).BoundedFormulaω Empty m} (t : Fin m ↪o ℕ) {n : ℕ} {χ : (localColim s₀).BoundedFormulaω Empty n} (hχ : ⟨n, χ⟩ ∈ ΓEMlocal s₀) (u : Fin n ↪o ℕ) (hsem : ∀ (σ h : ℕ → M), realizeWith σ h (schemaLift ψ t) Empty.elim Fin.elim0 → realizeWith σ h (schemaLift χ u) Empty.elim Fin.elim0) (hmem : schemaLift ψ t ∈ schemaCompletionTheory (schemaEnumeration s₀) hM) : schemaLift χ u ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

Directional semantic sign transport. If every body interpretation realizing schemaLift ψ t also realizes schemaLift χ u, then theory membership transfers — only the TARGET's universe membership is needed (to ask for its sign). If the target were negative, one body would realize the source and the negated target, contradicting the implication.

theorem FirstOrder.Language.schema_mem_iff_of_semantic_iff {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {m : ℕ} {ψ : (localColim s₀).BoundedFormulaω Empty m} (hψ : ⟨m, ψ⟩ ∈ ΓEMlocal s₀) (t : Fin m ↪o ℕ) {n : ℕ} {χ : (localColim s₀).BoundedFormulaω Empty n} (hχ : ⟨n, χ⟩ ∈ ΓEMlocal s₀) (u : Fin n ↪o ℕ) (hsem : ∀ (σ h : ℕ → M), realizeWith σ h (schemaLift ψ t) Empty.elim Fin.elim0 ↔ realizeWith σ h (schemaLift χ u) Empty.elim Fin.elim0) : schemaLift ψ t ∈ schemaCompletionTheory (schemaEnumeration s₀) hM ↔ schemaLift χ u ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

Semantic sign transport. Two universe sentences semantically equivalent under every body interpretation receive the same sign from the completed theory. The workhorse for normalizing between schemaFormulaSentence, the atomic sentences, and canonical deForms in the truth lemma — one body extraction per equivalence, no quotient induction.