Layer 7b, checkpoint 1: the countable schema sentence universe

The ω-stage Henkin/template completion (Layer 7) is carried out at the schema level, over the canonical countable index J := ℕ (the indiscernible-sequence positions d₀, d₁, …), where the sentence set the completion ranges over is genuinely countable — unlike the uncountable L'[[J]]-constant instances for arbitrary J that defeated the Layer-6c Zorn maximal.

This file fixes the schema sentence universe: the set of (localColim s₀)[[ℕ]]-sentences the enumeration in checkpoint 3 will decide. A crucial simplification, established in SchemaOmegaWitness, drives the shape: the target witness property TailTemplateOmegaWitnessed/OmegaCompleteForColim has only iSup/iInf clauses, no existential (the local-EM de-substituted formulas are already Skolemized). Since ΓlocalColim — hence ΓEMlocal — is closed under iSup/iInf components (iSup_component_mem_ΓlocalColim), every disjunct a completion might choose as a witness is already a member of the seed family. So the universe is exactly the templateSentence instantiations of the ΓEMlocal members at ℕ-tuples:

• the seed family ΓEMlocal s₀ is countable (ΓEMlocal_countable);
• for each member ⟨m, φ⟩, the increasing ℕ-tuples t : Fin m ↪o ℕ form a countable type (they inject into Fin m → ℕ);
• templateSentence φ t is the L[[ℕ]]-sentence "φ holds on d_{t 0}, …, d_{t (m-1)}".

schemaSentenceUniverse_countable is the checkpoint-1 payoff (the completion's decision list is enumerable); schemaSentenceUniverse_nonempty supplies the base point the enumeration needs. No completion, Zorn, term model, or realizeWith bridge appears here — this checkpoint only pins the countable substrate.

instance FirstOrder.Language.instCountableFinOrderEmbNat (m : ℕ) : Countable (Fin m ↪o ℕ)

Increasing ℕ-tuples of any fixed length are countable: the coercion to Fin m → ℕ is injective, and Fin m → ℕ is countable.

def FirstOrder.Language.schemaSentenceUniverse (s₀ : LocalStage) : Set ((localColim s₀).withConstants ℕ).Sentenceω

The schema sentence universe. Over the base language (localColim s₀)[[ℕ]] (ℕ the canonical indiscernible-sequence positions), the set of templateSentence φ t — "φ holds on the constants d_{t 0}, …, d_{t (m-1)}" — as ⟨m, φ⟩ ranges over the colimit atom/connective family ΓEMlocal s₀ and t over the increasing ℕ-tuples of length m. This is the countable decision list of the ω-stage completion; its iSup/iInf witnesses stay inside it because ΓEMlocal ⊇ ΓlocalColim is component-closed.

Equations

• FirstOrder.Language.schemaSentenceUniverse s₀ = ⋃ mφ ∈ FirstOrder.Language.ΓEMlocal s₀, Set.range fun (t : Fin mφ.fst ↪o ℕ) => FirstOrder.Language.Lomega1omegaTemplate.templateSentence mφ.snd t

theorem FirstOrder.Language.schemaSentenceUniverse_countable {s₀ : LocalStage} : (schemaSentenceUniverse s₀).Countable

Checkpoint 1. The schema sentence universe is countable — a countable union (over the countable seed family ΓEMlocal s₀) of ranges of maps out of the countable tuple types. This is what makes the ω-enumeration of the completion possible.

def FirstOrder.Language.stdTuple (m : ℕ) : Fin m ↪o ℕ

A canonical length-m increasing ℕ-tuple: the inclusion Fin m ↪ ℕ by value, which is strictly monotone. Used to base-point the schema universe.

Equations

• FirstOrder.Language.stdTuple m = OrderEmbedding.ofStrictMono (fun (i : Fin m) => ↑i) ⋯

theorem FirstOrder.Language.schemaSentenceUniverse_nonempty {s₀ : LocalStage} : (schemaSentenceUniverse s₀).Nonempty

The schema sentence universe is nonempty: the seed family is nonempty (ΓEMlocal_nonempty) and every arity admits the standard tuple, so the corresponding templateSentence is a member. Supplies the base point the enumeration in checkpoint 3 needs.

Checkpoint 2, step 1: the template-realization bridge

Connects MarkerStage's realizeWith (over the double Henkin expansion ((L''[[J]])[[ℕ]])) to the templateSentence semantics: the schema sentence templateSentence ψ t, lifted into the Marker language along the Henkin inclusion, is realizeWith-true under a skeleton interpretation σ exactly when ψ holds on the σ-images i ↦ σ (t i) of its constants. The Henkin layer is inert (no Henkin constants occur). This is the semantic content the base certification (step 3) and the seed agreement (7c) both consume. Stated generically in L''/J, so the two constantsOn instances of realizeWith stay unambiguous (as at its definition site).

theorem FirstOrder.Language.realizeWith_templateSentence {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {n : ℕ} (ψ : L''.BoundedFormulaω Empty n) (t : Fin n ↪o J) : realizeWith σ h (BoundedFormulaω.mapLanguage ((L''.withConstants J).lhomWithConstants ℕ) (Lomega1omegaTemplate.templateSentence ψ t)) Empty.elim Fin.elim0 ↔ ψ.Realize Empty.elim fun (i : Fin n) => σ (t i)

The template-realization bridge. templateSentence ψ t (over L''[[J]]), lifted into the Marker double expansion ((L''[[J]])[[ℕ]]) along the Henkin inclusion, realizes under a skeleton interpretation σ : J → M and any Henkin interpretation h : ℕ → M iff ψ holds on the tuple i ↦ σ (t i). Composes sentenceRealize_iff_realizeWith, realize_mapLanguage (the Henkin inclusion is an expansion, withConstants_expansion), and the existing realize_templateSentence.

Checkpoint 2: the empty base is Marker-consistent

The ω-stage completion (checkpoint 3) starts from the empty theory and decides every schema sentence's sign via the already-proved MarkerHenkinConsistent.extension (which internally homogenizes through markerStage_homogeneous). Since schemaSentenceUniverse is a decision list — its canonical atoms include both true and false instances (e.g. x₀ = x₁) — the base is NOT "all universe sentences are true"; it is the trivially-realizable empty fragment. The Morley seed {φ, x₀ ≠ x₁} needs no explicit seeding: extension is forced to pick φ (its negation is incompatible with M ⊨ φ) and distinctness (its negation is incompatible with the strictly increasing skeleton interpretations).

theorem FirstOrder.Language.markerHenkinConsistent_empty {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) : MarkerHenkinConsistent M ∅

Checkpoint 2. The empty fragment is MarkerHenkinConsistent M for any source M of size ≥ ℶ_ω₁: at every level β < ω₁ the body is the trivial certificate over the (ℶ_β)⁺-suborder e supplied by markerStage_homogeneous at empty arity, with no members to realize. This is the starting point the ω-stage extension/iSup_choice chain builds on.

Checkpoint 3a: the lifted universe and its FSentence membership

The ω-stage completion runs over ((localColim s₀)[[ℕ]])[[ℕ]] (FSentence), so the universe must be lifted along the same Henkin inclusion as the bridge. Two functionsIn-under-mapLanguage facts (absent from the existing relabel/subst/openBounds API) drive the constant-support computation: lifting sends every function symbol to its Sum.inl image, so it produces no Henkin constants and preserves the skeleton-constant support. A lifted templateSentence ψ t then has finite constant support image t (and empty Henkin support) — regardless of how many base function symbols the (possibly iSup-branching) ψ uses, because HasFiniteConstSupport bounds only the constant symbols, never all of functionsIn.

theorem FirstOrder.Language.henkinConstsIn_mapLanguage {L'' : Language} {J α : Type} {n : ℕ} (τ : (L''.withConstants J).BoundedFormulaω α n) : henkinConstsIn (BoundedFormulaω.mapLanguage ((L''.withConstants J).lhomWithConstants ℕ) τ) = ∅

The Henkin inclusion (L''[[J]]) →ᴸ ((L''[[J]])[[ℕ]]) sends every function symbol to its Sum.inl image; hence a lifted formula has no Henkin constants.

theorem FirstOrder.Language.expJConstsIn_mapLanguage {L'' : Language} {J α : Type} {n : ℕ} (τ : (L''.withConstants J).BoundedFormulaω α n) : expJConstsIn (BoundedFormulaω.mapLanguage ((L''.withConstants J).lhomWithConstants ℕ) τ) = sentenceJConsts τ

The Henkin inclusion preserves the skeleton (J) constant support: the expansion J-constants of a lifted formula are exactly the J-constants of the original.

theorem FirstOrder.Language.sentenceJConsts_templateSentence {L'' : Language} {J : Type} [LinearOrder J] {n : ℕ} (ψ : L''.BoundedFormulaω Empty n) (t : Fin n ↪o J) : sentenceJConsts (Lomega1omegaTemplate.templateSentence ψ t) ⊆ Set.range ⇑t

The only J-constants of a templateSentence ψ t are the tuple's constants: substitution introduces exactly {t 0, …, t (n-1)} and the mapLanguaged body contributes only base (Sum.inl) symbols.

theorem FirstOrder.Language.hasFiniteConstSupport_mapLanguage_templateSentence {L'' : Language} {J : Type} [LinearOrder J] {n : ℕ} (ψ : L''.BoundedFormulaω Empty n) (t : Fin n ↪o J) : HasFiniteConstSupport (BoundedFormulaω.mapLanguage ((L''.withConstants J).lhomWithConstants ℕ) (Lomega1omegaTemplate.templateSentence ψ t))

Every lifted templateSentence is an FSentence. Its expansion J-support is the finite tuple image image t, and its Henkin support is empty.

def FirstOrder.Language.schemaFSentenceUniverse (s₀ : LocalStage) : Set FSentence

The lifted schema universe, as a set of FSentences over the Marker language ((localColim s₀)[[ℕ]])[[ℕ]]: each schema sentence templateSentence ψ t (⟨m, ψ⟩ ∈ ΓEMlocal), lifted along the Henkin inclusion and packaged with its finite-support proof. This is the enumeration domain the ω-stage completion (checkpoint 3b) decides.

Equations

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

theorem FirstOrder.Language.schemaFSentenceUniverse_countable {s₀ : LocalStage} : (schemaFSentenceUniverse s₀).Countable

Checkpoint 3a. The lifted schema FSentence universe is countable — the enumeration the completion needs exists.

theorem FirstOrder.Language.schemaFSentenceUniverse_nonempty {s₀ : LocalStage} : (schemaFSentenceUniverse s₀).Nonempty

The lifted schema FSentence universe is nonempty (base point for the enumeration).

Checkpoint 3b: the ω-stage completion (subtype recursion)

A constructive Henkin enumeration over ρ : ℕ → FSentence. Each stageStep decides ρ n via extension (branching on decidable consistency of the positive insert — extension's ∨ is a Prop and cannot eliminate into the Subtype), and, opportunistically and locally, adjoins the connective witness of the decided sign: a positive iSup gets a disjunct via iSup_choice, a negative iInf gets a refuted conjunct via neg_iInf_choice. The step carries the balanced disjunction (positive ∧ iSup-witnessed) ∨ (negative ∧ neg-iInf-witnessed), so the per-stage facts 3c consumes are projections — no global classifier, no "φ ∉ F" discharge. The negative witness is NOT recoverable from finite consistency after the theory is formed (a finite fragment's body can falsify a component the fragment does not mention, so the failing component drifts with the body); it must be pinned here, at decision time.

noncomputable def FirstOrder.Language.stageStep {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] (ρ : ℕ → FSentence) (Fp : { F : Finset (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω // MarkerHenkinConsistent M F }) (n : ℕ) : { G : Finset (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω // MarkerHenkinConsistent M G ∧ ↑Fp ⊆ G ∧ ((↑(ρ n) ∈ G ∧ ∀ (φs : ℕ → (((localColim s₀).withConstants ℕ).withConstants ℕ).BoundedFormulaω Empty 0), ↑(ρ n) = BoundedFormulaω.iSup φs → ∃ (k : ℕ), φs k ∈ G) ∨ BoundedFormulaω.not ↑(ρ n) ∈ G ∧ ∀ (φs : ℕ → (((localColim s₀).withConstants ℕ).withConstants ℕ).BoundedFormulaω Empty 0), ↑(ρ n) = BoundedFormulaω.iInf φs → ∃ (k : ℕ), (φs k).not ∈ G) }

The stage step. Given a consistent finite stage Fp, decide ρ n and (locally) witness the decided sign's connective: a positive iSup gets a disjunct, a negative iInf a refuted conjunct. Returns the next stage with consistency, monotonicity, and the balanced decision record (positive ∧ iSup-witnessed) ∨ (negative ∧ neg-iInf-witnessed).

Equations

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

noncomputable def FirstOrder.Language.schemaCompletionStage {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) : ℕ → { F : Finset (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω // MarkerHenkinConsistent M F }

The completion stages. T 0 = ∅; T (n+1) is the stageStep of T n.

Equations

• FirstOrder.Language.schemaCompletionStage ρ hM 0 = ⟨∅, ⋯⟩
• FirstOrder.Language.schemaCompletionStage ρ hM n.succ = ⟨↑(FirstOrder.Language.stageStep ρ (FirstOrder.Language.schemaCompletionStage ρ hM n) n), ⋯⟩

theorem FirstOrder.Language.markerHenkinConsistent_not_mem_and_not_mem {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] {F : Finset (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) (τ : (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω) : ¬(τ ∈ F ∧ BoundedFormulaω.not τ ∈ F)

C0 at the consistency level: a MarkerHenkinConsistent fragment contains no sentence together with its negation (a body at some level realizes both, contradicting realizeWith_not).

theorem FirstOrder.Language.schemaCompletionStage_consistent {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (n : ℕ) : MarkerHenkinConsistent M ↑(schemaCompletionStage ρ hM n)

Each stage is MarkerHenkinConsistent (built into the subtype).

theorem FirstOrder.Language.schemaCompletionStage_subset_succ {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (n : ℕ) : ↑(schemaCompletionStage ρ hM n) ⊆ ↑(schemaCompletionStage ρ hM (n + 1))

One-step monotonicity: a stage is contained in its successor.

theorem FirstOrder.Language.schemaCompletionStage_mono {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {m n : ℕ} (h : m ≤ n) : ↑(schemaCompletionStage ρ hM m) ⊆ ↑(schemaCompletionStage ρ hM n)

Monotonicity of the completion chain.

theorem FirstOrder.Language.schemaCompletionStage_decides {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (n : ℕ) : ↑(ρ n) ∈ ↑(schemaCompletionStage ρ hM (n + 1)) ∨ BoundedFormulaω.not ↑(ρ n) ∈ ↑(schemaCompletionStage ρ hM (n + 1))

Stage n decides ρ n: after stage n+1, either (ρ n).1 or its negation is present.

theorem FirstOrder.Language.schemaCompletionStage_witness {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (n : ℕ) {φs : ℕ → (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω} (hiSup : ↑(ρ n) = BoundedFormulaω.iSup φs) (hpos : ↑(ρ n) ∈ ↑(schemaCompletionStage ρ hM (n + 1))) : ∃ (k : ℕ), φs k ∈ ↑(schemaCompletionStage ρ hM (n + 1))

Stage n witnesses a positive iSup: if (ρ n).1 is iSup φs and lands positively in stage n+1, some component φs k is present too.

theorem FirstOrder.Language.schemaCompletionStage_neg_iInf_witness {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (n : ℕ) {φs : ℕ → (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω} (hiInf : ↑(ρ n) = BoundedFormulaω.iInf φs) (hneg : BoundedFormulaω.not ↑(ρ n) ∈ ↑(schemaCompletionStage ρ hM (n + 1))) : ∃ (k : ℕ), BoundedFormulaω.not (φs k) ∈ ↑(schemaCompletionStage ρ hM (n + 1))

Stage n witnesses a negative iInf: if (ρ n).1 is iInf φs and its negation lands in stage n+1, some refuted component (φs k).not is present too. The mirror of schemaCompletionStage_witness, projecting the negative half of the balanced decision record.

Checkpoint 3c: the union theory

The completed theory T = ⋃ₙ (schemaCompletionStage ρ hM n).1, kept as a raw set of Marker sentences. Finite-character consistency (a finite subset lands in one stage), completeness on the universe (each ρ n decided at its stage), and — the iSup-witness closure — will bundle into SchemaCompletionTheorySpec.

noncomputable def FirstOrder.Language.schemaEnumeration (s₀ : LocalStage) : ℕ → FSentence

The canonical enumeration of the schema universe (from countable + nonempty).

Equations

• FirstOrder.Language.schemaEnumeration s₀ = ⋯.choose

theorem FirstOrder.Language.schemaEnumeration_range {s₀ : LocalStage} : Set.range (schemaEnumeration s₀) = schemaFSentenceUniverse s₀

def FirstOrder.Language.schemaCompletionTheory {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) : Set (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω

The completed theory (raw set of Marker sentences), the union of the completion stages.

Equations

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

theorem FirstOrder.Language.finite_subset_stage {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (F : Finset (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω) : (∀ τ ∈ F, τ ∈ schemaCompletionTheory ρ hM) → ∃ (N : ℕ), F ⊆ ↑(schemaCompletionStage ρ hM N)

Step 2. A finite subset of the completed theory lands in a single stage.

theorem FirstOrder.Language.schemaCompletionTheory_finite_consistent {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (F : Finset (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω) (hF : ∀ τ ∈ F, τ ∈ schemaCompletionTheory ρ hM) : MarkerHenkinConsistent M F

Finite-character consistency: every finite subset of the completed theory is MarkerHenkinConsistent.

theorem FirstOrder.Language.schemaCompletionTheory_complete {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (ρ : ℕ → FSentence) (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (hρrange : Set.range ρ = schemaFSentenceUniverse s₀) (τ : FSentence) (hτ : τ ∈ schemaFSentenceUniverse s₀) : ↑τ ∈ schemaCompletionTheory ρ hM ∨ BoundedFormulaω.not ↑τ ∈ schemaCompletionTheory ρ hM

Step 3 — completeness on the universe: every schema-universe sentence is decided by the completed theory (using range ρ = universe).

theorem FirstOrder.Language.schemaCompletionTheory_iSup_witness_localColim {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {m : ℕ} {φs : ℕ → (localColim s₀).BoundedFormulaω Empty m} (hmem : ⟨m, BoundedFormulaω.iSup φs⟩ ∈ ΓlocalColim s₀) (t : Fin m ↪o ℕ) (hT : BoundedFormulaω.mapLanguage (((localColim s₀).withConstants ℕ).lhomWithConstants ℕ) (Lomega1omegaTemplate.templateSentence (BoundedFormulaω.iSup φs) t) ∈ schemaCompletionTheory (schemaEnumeration s₀) hM) : ∃ (k : ℕ), BoundedFormulaω.mapLanguage (((localColim s₀).withConstants ℕ).lhomWithConstants ℕ) (Lomega1omegaTemplate.templateSentence (φs k) t) ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

Step 4/5 — the restricted iSup-witness closure. For a ΓlocalColim disjunction ⟨m, iSup φs⟩ and any tuple t, if the lifted templateSentence (iSup φs) t is in the completed theory (over the canonical enumeration), then some component's lifted templateSentence (φs k) t is too. This is exactly the clause TailTemplateOmegaWitnessed/R1 consumes — no full ΓEMlocal component closure, no deForm case. The lifted templateSentence distributes over iSup (rfl); the sentence is a universe member (via ΓlocalColim ⊆ ΓEMlocal), so it is some ρ j, decided at stage j — positively (a negative decision would put both it and its negation in a common later stage, contradicting markerHenkinConsistent_not_mem_and_not_mem); schemaCompletionStage_witness then supplies the component.

theorem FirstOrder.Language.schemaCompletionTheory_iSup_witness_of_universe {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (τ : FSentence) (hτ : τ ∈ schemaFSentenceUniverse s₀) {φs : ℕ → (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω} (hiSup : ↑τ = BoundedFormulaω.iSup φs) (hpos : ↑τ ∈ schemaCompletionTheory (schemaEnumeration s₀) hM) : ∃ (k : ℕ), φs k ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

The iSup-witness closure on the universe. For a universe member τ of iSup shape present in the completed theory (over the canonical enumeration), some component is present too — read off the stage that decided τ, as in schemaCompletionTheory_iSup_witness_localColim but generic in the universe member (the canonical-deForm closure in 5b-2 instantiates it).

theorem FirstOrder.Language.schemaCompletionTheory_neg_iInf_witness_of_universe {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) (τ : FSentence) (hτ : τ ∈ schemaFSentenceUniverse s₀) {φs : ℕ → (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω} (hiInf : ↑τ = BoundedFormulaω.iInf φs) (hneg : BoundedFormulaω.not ↑τ ∈ schemaCompletionTheory (schemaEnumeration s₀) hM) : ∃ (k : ℕ), BoundedFormulaω.not (φs k) ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

The negative iInf-witness closure on the universe. For a universe member τ of iInf shape whose negation is in the completed theory (over the canonical enumeration), some refuted component (φs k).not is in the theory too. This is the direction the restricted truth lemma's iInf case needs ((∀ k, ⊨ φs k) → ⊨ iInf φs, contrapositively), and it is NOT derivable from finite consistency after the theory is formed — the failing component would drift with the certificate body. It is read off the stage that decided τ, exactly as in schemaCompletionTheory_iSup_witness_localColim.

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

Checkpoint 3c bundle. The three properties of the completed schema theory over the canonical enumeration schemaEnumeration s₀: finite-character consistency, completeness on the schema universe, and the ΓlocalColim-restricted iSup-witness closure. Bundling keeps checkpoints 4/5 from re-threading ρ, the range fact, and monotonicity.

• finite_consistent (F : Finset (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω) : (∀ τ ∈ F, τ ∈ schemaCompletionTheory (schemaEnumeration s₀) hM) → MarkerHenkinConsistent M F

  Every finite subset of the completed theory is MarkerHenkinConsistent.

• complete_on_universe (τ : FSentence) : τ ∈ schemaFSentenceUniverse s₀ → ↑τ ∈ schemaCompletionTheory (schemaEnumeration s₀) hM ∨ BoundedFormulaω.not ↑τ ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

  Every schema-universe sentence is decided by the completed theory.

• iSup_witness_localColim {m : ℕ} {φs : ℕ → (localColim s₀).BoundedFormulaω Empty m} : ⟨m, BoundedFormulaω.iSup φs⟩ ∈ ΓlocalColim s₀ → ∀ (t : Fin m ↪o ℕ), BoundedFormulaω.mapLanguage (((localColim s₀).withConstants ℕ).lhomWithConstants ℕ) (Lomega1omegaTemplate.templateSentence (BoundedFormulaω.iSup φs) t) ∈ schemaCompletionTheory (schemaEnumeration s₀) hM → ∃ (k : ℕ), BoundedFormulaω.mapLanguage (((localColim s₀).withConstants ℕ).lhomWithConstants ℕ) (Lomega1omegaTemplate.templateSentence (φs k) t) ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

  A ΓlocalColim disjunction present in the theory has a component present.

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

Checkpoint 3c complete: the completed schema theory over schemaEnumeration s₀ satisfies the bundle — the witnessed schema object the extraction (checkpoint 5) consumes.

Checkpoint 5b-1, part 1: the finite interpolation engine

Tuple uniformity (part 2) needs, for two length-m increasing tuples t t' into ℕ and ONE certificate body, two admissible skeleton interpretations σ₁ σ₂ whose tuple images agree: σ₁ ∘ t = σ₂ ∘ t'. The engine is a global equalizer on ℕ: strictly monotone q q' : ℕ → ℕ sending the anchors p i/p' i to the common value p i + p' i — q shifts by the largest passed p'-anchor (a Finset.sup over a filter), so no piecewise case analysis is needed. exists_admissible_pair threads the equalized values through a Fin K-suborder of the (infinite) certificate domain. Crucially, MarkerHenkinBody constrains σ only ON the support S, so the tuples need not lie in S: they enter only the auxiliary bounding set that picks K — the Marker support itself is never enlarged.

theorem FirstOrder.Language.exists_strictMono_equalizer {m : ℕ} (p p' : Fin m → ℕ) (hp : StrictMono p) (hp' : StrictMono p') : ∃ (q : ℕ → ℕ) (q' : ℕ → ℕ), StrictMono q ∧ StrictMono q' ∧ ∀ (i : Fin m), q (p i) = q' (p' i)

The global equalizer. Two strictly monotone tuples p p' : Fin m → ℕ are equalized by strictly monotone q q' : ℕ → ℕ: q (p i) = q' (p' i) (both anchors land at p i + p' i).

theorem FirstOrder.Language.exists_admissible_pair {M D : Type} [LinearOrder M] [LinearOrder D] [Infinite D] {m : ℕ} (S : Finset ℕ) (e : D ↪o M) (t t' : Fin m ↪o ℕ) (dflt : M) : ∃ (σ₁ : ℕ → M) (σ₂ : ℕ → M), StrictMonoOn σ₁ ↑S ∧ (∀ j ∈ S, σ₁ j ∈ Set.range ⇑e) ∧ StrictMonoOn σ₂ ↑S ∧ (∀ j ∈ S, σ₂ j ∈ Set.range ⇑e) ∧ ∀ (i : Fin m), σ₁ (t i) = σ₂ (t' i)

The admissible pair. For a finite support S, a suborder e : D ↪o M with infinite domain, and two increasing tuples t t' : Fin m ↪o ℕ, there are skeleton interpretations σ₁ σ₂ : ℕ → M — each strictly monotone on S with S-values in range e (the MarkerHenkinBody admissibility) — whose tuple images agree: σ₁ ∘ t = σ₂ ∘ t'. This is what lets ONE certificate body be applied twice, once per tuple, in tuple uniformity.

Checkpoint 5b-1, part 2: tuple uniformity

The completed schema theory decides a template sentence's sign by its ΓEMlocal body alone, uniformly across the instantiating tuples: schemaLift ψ t ∈ Tσ ↔ schemaLift ψ t' ∈ Tσ. This is the internal form of Marker §5.2's indiscernibility-equivalence axioms, and it is what makes the term model's canonical sequence genuinely indiscernible for the completed schema (5b-3).

The proof is the honest two-interpretation argument: if ψ t is in and ψ t' is out, then (by completeness on the universe) {schemaLift ψ u, (schemaLift ψ v).not} is a finite subset of the theory, hence MarkerHenkinConsistent; its ONE certificate body is universal over admissible skeleton interpretations, so it applies separately to the exists_admissible_pair pair σ₁, σ₂ — the first realizes ψ on σ₁ ∘ t, the second refutes ψ on σ₂ ∘ t', and those tuples are EQUAL. No single interpretation is asked to equalize both tuples (strictness would forbid it); no Henkin witness dependence arises on this single-expansion path.

@[reducible, inline]

abbrev FirstOrder.Language.schemaLift {s₀ : LocalStage} {m : ℕ} (ψ : (localColim s₀).BoundedFormulaω Empty m) (t : Fin m ↪o ℕ) : (((localColim s₀).withConstants ℕ).withConstants ℕ).Sentenceω

The schema lift: a template sentence over (localColim s₀)[[ℕ]], lifted along the Henkin inclusion into the Marker double expansion — the form in which the completed theory holds the schema universe. Public API: 5b-3's restricted truth lemma states its atomic clauses in exactly these terms.

Equations

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

theorem FirstOrder.Language.schemaLift_mem_universe {s₀ : LocalStage} {m : ℕ} {ψ : (localColim s₀).BoundedFormulaω Empty m} (hψ : ⟨m, ψ⟩ ∈ ΓEMlocal s₀) (t : Fin m ↪o ℕ) : ⟨schemaLift ψ t, ⋯⟩ ∈ schemaFSentenceUniverse s₀

Every schema lift of a ΓEMlocal member is a universe member (with its canonical finite-support proof).

theorem FirstOrder.Language.schemaCompletionTheory_tuple_uniform {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 t' : Fin m ↪o ℕ) : schemaLift ψ t ∈ schemaCompletionTheory (schemaEnumeration s₀) hM ↔ schemaLift ψ t' ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

Checkpoint 5b-1 — tuple uniformity. The completed schema theory gives every ΓEMlocal body a tuple-independent sign: for same-arity increasing tuples t t', the lifted templateSentence ψ t is in the theory iff the lifted templateSentence ψ t' is.

Checkpoint 5b-2: connective witnesses for canonical deForms

TailTemplateOmegaWitnessed — the 5b-3 target — is stated on canonDeForm (localColim s₀) φ g, not on the raw ΓlocalColim connectives, so the completed theory's witness closures must be exposed in exactly those terms. Both directions are corollaries of the universe-level closures: canonDeForm and schemaLift each distribute over iSup/iInf definitionally, and canonDeForm_mem_ΓEMlocal puts the deForm in the universe. The negative direction is the whole point of the completion repair: the fixed refuted conjunct was pinned at decision time and is simply read off here.

theorem FirstOrder.Language.schemaCompletionTheory_iSup_witness_canonDeForm {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {m : ℕ} {φs : ℕ → (localColim s₀).BoundedFormulaω Empty m} (hmem : ⟨m, BoundedFormulaω.iSup φs⟩ ∈ ΓlocalColim s₀) {p : ℕ} (g : Fin m → (localColim s₀).Term (Fin p)) (t : Fin p ↪o ℕ) (hT : schemaLift ((localColim s₀).canonDeForm (BoundedFormulaω.iSup φs) g) t ∈ schemaCompletionTheory (schemaEnumeration s₀) hM) : ∃ (k : ℕ), schemaLift ((localColim s₀).canonDeForm (φs k) g) t ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

Positive iSup witness, canonical-deForm form. If the lifted template sentence of a ΓlocalColim disjunction's deForm is in the completed theory, so is some component's.

theorem FirstOrder.Language.schemaCompletionTheory_neg_iInf_witness_canonDeForm {s₀ : LocalStage} {M : Type} [(localColim s₀).Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.beth (Ordinal.omega 1) ≤ Cardinal.mk M) {m : ℕ} {φs : ℕ → (localColim s₀).BoundedFormulaω Empty m} (hmem : ⟨m, BoundedFormulaω.iInf φs⟩ ∈ ΓlocalColim s₀) {p : ℕ} (g : Fin m → (localColim s₀).Term (Fin p)) (t : Fin p ↪o ℕ) (hneg : BoundedFormulaω.not (schemaLift ((localColim s₀).canonDeForm (BoundedFormulaω.iInf φs) g) t) ∈ schemaCompletionTheory (schemaEnumeration s₀) hM) : ∃ (k : ℕ), BoundedFormulaω.not (schemaLift ((localColim s₀).canonDeForm (φs k) g) t) ∈ schemaCompletionTheory (schemaEnumeration s₀) hM

Negative iInf witness, canonical-deForm form. If the negation of the lifted template sentence of a ΓlocalColim conjunction's deForm is in the completed theory, some component's negation is too — the fixed refuted conjunct the restricted truth lemma's iInf case consumes.