The Marker stage: finite-fragment support extraction and Erdős–Rado certification

First layer of the template/consistency-property reshape of the Morley–Hanf chain (the replacement for the ZFC-refutable in-M extraction ladder — see the audit fences on PureColoringHypothesis/MorleyHanfExtraction in Conditional/MorleyHanfTransfer.lean). Following Marker, Lectures on Infinitary Model Theory §5.2, the consistency-property route certifies each finite fragment of an L'[[J]] template/constant theory by a large homogeneous set in the source model, with the indiscernible sequence materializing only in the model built by Model Existence.

This file provides the syntactic/combinatorial bridge between "finite fragment of a constant theory" and "finite-arity Erdős–Rado approximation":

• a finite fragment is presented by its index data — a finite family of pairs (fml p : L'.BoundedFormulaω Empty (ar p), tup p : Fin (ar p) ↪o J) (per the template machinery in Methods/EM/Realization.lean, membership in a template theory carries exactly this witness data, so no syntactic support extraction is ever needed);
• exists_markerSupport_factor — collect the finite J-constant support of the family, enumerate it as enum : Fin k ↪o J, and factor every tup p through enum (via exists_orderEmbedding_factor);
• markerStage_homogeneous — pull the family back to a single arity-k truth-vector coloring over the source model and apply finiteArityHomogeneousUpTo_beth_stage: for every α < ω₁, a source of size ≥ ℶ_{ω₁} yields a (ℶ_α)⁺-suborder on which the truth vector of the whole fragment is tuple-independent.

The per-α conclusion (available for every α < ω₁ at once) is the Marker schedule.

Layer 2: the certification predicates and their closure calculus

Toward the Marker consistency property, this file also provides the candidate member predicate and its easy closure lemmas:

• sentenceJConsts — the syntactic J-constant support of an L'[[J]]-sentence (a Set J carved out of functionsIn; only countable in general, finite exactly for the sentences the construction certifies — support finiteness is demanded by the predicate, never computed);
• MarkerFiniteCert M α F — a finite set of sentences is certified at level α: a common finite support S, a (ℶ_α)⁺-suborder e of M, and satisfaction of every member under every constant interpretation that is increasing on S into e's range;
• MarkerCofinalConsistent M Sset — every finite subset is certified at cofinally many α < ω₁ (finite character makes weakening and chain closure pleasant);
• the closure lemmas that need no uniform countable choice: weakening, chain closure, the C0 pair (no falsum, no contradiction), C2 (double negation), C3 (conjunction components), C4' (negated-disjunction components) — each by replacing the derived sentence with its trigger inside the certified fragment (MarkerCofinalConsistent.extend_of_semantic) and pushing pointwise realize lemmas through the same interpretations;
• exists_uniform_of_cofinal_countable — the ω₁-pigeonhole engine (ω₁ is regular, so a countably-colored cofinal α-schedule has a monochromatic cofinal subschedule);
• MarkerISupUniform — the stated hard test: does ⋁ᵢ φᵢ ∈ Sset yield ONE disjunct k with Sset ∪ {φs k} still cofinally consistent? Per finite fragment F and level α, re-homogenization + the pigeonhole produce k(F); the open question is uniformizing over ALL finite F ⊆ Sset — a directed intersection of antitone nonempty subsets of ℕ, which is NOT automatic. If provable, markerConsistencyPropertyEq is mostly assembly; if not, the fallback is a finite-member consistency notion with its own Henkin/model-existence adapter (the existing ConsistencyPropertyEq API also demands extension for ARBITRARY sentences, which certification cannot supply for sentences of infinite support — another reason the finite-member adapter may be the honest endpoint).

C7/Henkin witness design (SETTLED: Henkin constant expansion — see Layer 3): over a relational L', the closed L'[[J]]-terms are exactly the J-constants, so quantifier witnesses must be fresh constants; a fresh J-constant would have to occupy a specific order-position that an arbitrary linear J need not offer, so witnesses live in a separate layer (L'[[J]])[[ℕ]] instead (henkinConst, henkinConstsIn, expJConstsIn), with the reduct lemma (Theoryω.model_reduct_of_expansion) returning the final model to L'[[J]]. The finite-member predicates over the expansion (MarkerHenkinCert, MarkerHenkinConsistent, Layer 5) avoid the arbitrary-set extension field and the global C4 uniformization entirely — the Henkin construction consumes finite members along its enumeration, per the classical Marker/Keisler shape. The realizeWith API (Layer 4) confines all structure instances to two definition bodies; every closure rule is stated through it. The choice-free closure rules (C0/C1'/C2/C3/C4') are proved in Layer 5; remaining: the re-homogenization rules (C1, C3', C4 — per-member branch/index choice by coloring support tuples inside the certificate), C7 via a fresh witness index (enabled by the finite-Henkin-support invariant — see the Layer 5 audit note), then the Henkin construction/model-existence adapter decision.

theorem FirstOrder.Language.add_natCast_lt_omega_one {α : Ordinal.{0}} (hα : α < Ordinal.omega 1) (n : ℕ) : α + ↑n < Ordinal.omega 1

Every finite ordinal step stays below ω₁: if α < ω₁ then α + n < ω₁ for every natural n — the room the Marker α-schedule uses to absorb per-fragment ladder costs.

theorem FirstOrder.Language.exists_markerSupport_factor {J : Type u} [LinearOrder J] {m : ℕ} {ar : Fin m → ℕ} (tup : (p : Fin m) → Fin (ar p) ↪o J) : ∃ (k : ℕ) (enum : Fin k ↪o J) (r : (p : Fin m) → Fin (ar p) ↪o Fin k), (∀ (p : Fin m), RelEmbedding.trans (r p) enum = tup p) ∧ Set.range ⇑enum = ⋃ (p : Fin m), Set.range ⇑(tup p)

Support factorization for a finite constant-fragment. Given a finite family of J-constant tuples tup p : Fin (ar p) ↪o J (the index data of a finite fragment of an L'[[J]] constant theory), collect the finite support, enumerate it in increasing order as enum : Fin k ↪o J, and factor every tuple through the enumeration. The range equation identifies enum with the exact constant support of the fragment.

theorem FirstOrder.Language.markerStage_homogeneous {L' : Language} (M : Type) [L'.Structure M] [LinearOrder M] [WellFoundedLT M] (hM : Cardinal.mk M ≥ Cardinal.beth (Ordinal.omega 1)) (α : Ordinal.{0}) (hα : α < Ordinal.omega 1) {J : Type} [LinearOrder J] {m : ℕ} {ar : Fin m → ℕ} (fml : (p : Fin m) → L'.BoundedFormulaω Empty (ar p)) (tup : (p : Fin m) → Fin (ar p) ↪o J) : ∃ (k : ℕ) (enum : Fin k ↪o J) (r : (p : Fin m) → Fin (ar p) ↪o Fin k), (∀ (p : Fin m), RelEmbedding.trans (r p) enum = tup p) ∧ Set.range ⇑enum = ⋃ (p : Fin m), Set.range ⇑(tup p) ∧ ∃ (e : (Order.succ (Cardinal.beth α)).ord.ToType ↪o M), ∀ (u u' : Fin k ↪o M), (∀ (i : Fin k), u i ∈ Set.range ⇑e) → (∀ (i : Fin k), u' i ∈ Set.range ⇑e) → ∀ (p : Fin m), (fml p).Realize Empty.elim (⇑u ∘ ⇑(r p)) ↔ (fml p).Realize Empty.elim (⇑u' ∘ ⇑(r p))

The Marker-stage Erdős–Rado certification. A finite fragment of an L'[[J]] constant theory, presented by its index data (fml p, tup p), pulls back along the support factorization to a single arity-k truth-vector coloring over the source model M; for every α < ω₁, finiteArityHomogeneousUpTo_beth_stage then yields a (ℶ_α)⁺-suborder of M on which the truth of every formula of the fragment (at its own positions r p inside the support) is independent of the choice of increasing k-tuple.

This is the per-fragment certification of the Marker consistency property: available at every α < ω₁ simultaneously (the cofinal schedule), from the single hypothesis |M| ≥ ℶ_{ω₁} — per-α, per-finite-fragment approximations, never one ω₁-suborder homogeneous for all arities at once (that jump is ZFC-refutable; see the audit fences).

Layer 2: the certification predicates

def FirstOrder.Language.MarkerFiniteCert {L' : Language} {J : Type} [LinearOrder J] (M : Type) [L'.Structure M] [LinearOrder M] (α : Ordinal.{0}) (F : Set (L'.withConstants J).Sentenceω) : Prop

The per-level Marker certification of a finite fragment: a common finite constant support S, a (ℶ_α)⁺-suborder e of the (well-ordered) source M, and satisfaction of every member sentence under every constant interpretation that is strictly increasing on S with values in the range of e. This is Marker's "ℶ_α-large set realizing σ", stated semantically over interpretations so that the closure calculus needs no constructor inversion through the template pipeline.

Equations

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

def FirstOrder.Language.MarkerCofinalConsistent {L' : Language} {J : Type} [LinearOrder J] (M : Type) [L'.Structure M] [LinearOrder M] (Sset : Set (L'.withConstants J).Sentenceω) : Prop

The candidate Marker member predicate: every finite subfragment is certified at cofinally many levels α < ω₁. Finite character makes weakening and chain closure direct; the uniformization questions (MarkerISupUniform below) are exactly where it is honest.

Equations

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

theorem FirstOrder.Language.MarkerFiniteCert.mono {L' : Language} {J : Type} [LinearOrder J] {M : Type} [L'.Structure M] [LinearOrder M] {α : Ordinal.{0}} {F F' : Set (L'.withConstants J).Sentenceω} (hFF : F' ⊆ F) (h : MarkerFiniteCert M α F) : MarkerFiniteCert M α F'

Certification is monotone (downward-closed) in the fragment.

theorem FirstOrder.Language.MarkerCofinalConsistent.mono {L' : Language} {J : Type} [LinearOrder J] {M : Type} [L'.Structure M] [LinearOrder M] {Sset Sset' : Set (L'.withConstants J).Sentenceω} (hSS : Sset' ⊆ Sset) (h : MarkerCofinalConsistent M Sset) : MarkerCofinalConsistent M Sset'

Cofinal consistency is monotone (downward-closed) in the sentence set.

theorem FirstOrder.Language.MarkerCofinalConsistent.sUnion_chain {L' : Language} {J : Type} [LinearOrder J] {M : Type} [L'.Structure M] [LinearOrder M] {chain : Set (Set (L'.withConstants J).Sentenceω)} (hchain : ∀ T ∈ chain, MarkerCofinalConsistent M T) (hC : IsChain (fun (x1 x2 : Set (L'.withConstants J).Sentenceω) => x1 ⊆ x2) chain) (hne : chain.Nonempty) : MarkerCofinalConsistent M (⋃₀ chain)

Chain closure: the union of a nonempty ⊆-chain of cofinally consistent sets is cofinally consistent — a finite subfragment of the union lies in one chain member.

theorem FirstOrder.Language.exists_strictMonoOn_interp {J : Type} [LinearOrder J] {M : Type} [LinearOrder M] {α : Ordinal.{0}} (e : (Order.succ (Cardinal.beth α)).ord.ToType ↪o M) (S : Finset J) : ∃ (σ : J → M), StrictMonoOn σ ↑S ∧ ∀ j ∈ S, σ j ∈ Set.range ⇑e

There is always an interpretation that is increasing on a given finite support into the range of a (ℶ_α)⁺-suborder — the suborder's domain is infinite, so it contains increasing tuples of every finite length. Supplies the "evaluation point" for the C0 lemmas.

theorem FirstOrder.Language.MarkerFiniteCert.falsum_notMem {L' : Language} {J : Type} [LinearOrder J] {M : Type} [L'.Structure M] [LinearOrder M] {α : Ordinal.{0}} {F : Set (L'.withConstants J).Sentenceω} (h : MarkerFiniteCert M α F) : BoundedFormulaω.falsum ∉ F

C0 (no falsum): a certified fragment cannot contain ⊥ — an increasing interpretation exists and would have to realize it.

theorem FirstOrder.Language.MarkerFiniteCert.not_mem_and_not_mem {L' : Language} {J : Type} [LinearOrder J] {M : Type} [L'.Structure M] [LinearOrder M] {α : Ordinal.{0}} {F : Set (L'.withConstants J).Sentenceω} (h : MarkerFiniteCert M α F) (τ : (L'.withConstants J).Sentenceω) : ¬(τ ∈ F ∧ BoundedFormulaω.not τ ∈ F)

C0 (no contradiction): a certified fragment cannot contain both a sentence and its negation.

theorem FirstOrder.Language.MarkerCofinalConsistent.extend_of_semantic {L' : Language} {J : Type} [LinearOrder J] {M : Type} [L'.Structure M] [LinearOrder M] {Sset : Set (L'.withConstants J).Sentenceω} (h : MarkerCofinalConsistent M Sset) {trigger new : (L'.withConstants J).Sentenceω} (hmem : trigger ∈ Sset) (hsupp : sentenceJConsts new ⊆ sentenceJConsts trigger) (hder : ∀ (σ : J → M), trigger.Realize M → new.Realize M) : MarkerCofinalConsistent M (Sset ∪ {new})

The semantic extension scheme behind the choice-free closure conditions: if a trigger sentence of Sset semantically entails a new sentence pointwise (under every constant interpretation) and the constant support does not grow, then adjoining new preserves cofinal consistency — inside any finite subfragment, replace new by its trigger and reuse the certificate.

theorem FirstOrder.Language.MarkerCofinalConsistent.not_not {L' : Language} {J : Type} [LinearOrder J] {M : Type} [L'.Structure M] [LinearOrder M] {Sset : Set (L'.withConstants J).Sentenceω} (h : MarkerCofinalConsistent M Sset) {φ : (L'.withConstants J).Sentenceω} (hmem : (BoundedFormulaω.not φ).not ∈ Sset) : MarkerCofinalConsistent M (Sset ∪ {φ})

C2 (double negation): ¬¬φ ∈ Sset allows adjoining φ.

theorem FirstOrder.Language.MarkerCofinalConsistent.iInf_component {L' : Language} {J : Type} [LinearOrder J] {M : Type} [L'.Structure M] [LinearOrder M] {Sset : Set (L'.withConstants J).Sentenceω} (h : MarkerCofinalConsistent M Sset) {φs : ℕ → (L'.withConstants J).Sentenceω} (hmem : BoundedFormulaω.iInf φs ∈ Sset) (k : ℕ) : MarkerCofinalConsistent M (Sset ∪ {φs k})

C3 (conjunction components): ⋀ᵢ φᵢ ∈ Sset allows adjoining every component.

theorem FirstOrder.Language.MarkerCofinalConsistent.neg_iSup_component {L' : Language} {J : Type} [LinearOrder J] {M : Type} [L'.Structure M] [LinearOrder M] {Sset : Set (L'.withConstants J).Sentenceω} (h : MarkerCofinalConsistent M Sset) {φs : ℕ → (L'.withConstants J).Sentenceω} (hmem : (BoundedFormulaω.iSup φs).not ∈ Sset) (k : ℕ) : MarkerCofinalConsistent M (Sset ∪ {BoundedFormulaω.not (φs k)})

C4' (negated-disjunction components): ¬⋁ᵢ φᵢ ∈ Sset allows adjoining every negated component.

The ω₁-pigeonhole engine and the stated uniformization test

theorem FirstOrder.Language.exists_uniform_of_cofinal_countable {K : Type} [Countable K] (P : Ordinal.{0} → K → Prop) (h : ∀ β < Ordinal.omega 1, ∃ (α : Ordinal.{0}), β ≤ α ∧ α < Ordinal.omega 1 ∧ ∃ (k : K), P α k) : ∃ (k : K), ∀ β < Ordinal.omega 1, ∃ (α : Ordinal.{0}), β ≤ α ∧ α < Ordinal.omega 1 ∧ P α k

The cofinal-schedule pigeonhole: ω₁ is regular, so if cofinally many levels below ω₁ each carry a witness from a countable index type, ONE index works cofinally. This is the engine behind every uniformization step of the Marker consistency property (binary choices such as C1, and — if it suffices — the disjunction choice C4).

def FirstOrder.Language.MarkerISupUniform {L' : Language} {J : Type} [LinearOrder J] (M : Type) [L'.Structure M] [LinearOrder M] : Prop

The hard uniformization test (deliberately a named statement, not a theorem): does a disjunction in a cofinally consistent set admit ONE disjunct whose adjunction stays cofinally consistent? Per finite subfragment F and level α, re-homogenizing the disjunct index (countably many colors, ≤ ℶ_α) and pigeonholing the cofinal schedule (exists_uniform_of_cofinal_countable) produce a per-F disjunct k(F); the open content is uniformizing over ALL finite F ⊆ Sset — a directed intersection of antitone nonempty subsets of ℕ, which is not automatic. If this holds, the Marker consistency property (ConsistencyPropertyEq's C4_iSup) is mostly assembly; if it fails, the honest route is a finite-member consistency notion with its own Henkin/model-existence adapter (see the module docstring, including the extension-field obstruction).

Equations

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

Layer 3: the Henkin-witness substrate

C7 design decision (settled): Henkin constant expansion. Quantifier witnesses live in a separate withConstants layer (L'[[J]])[[ℕ]], NOT among the J-constants: an arbitrary linear J need not have an element in the order-gap a witness would require (and MorleySeedTailTemplateRealizable quantifies over every linear J); a relational L' provides no closed terms beyond constants, so witnesses cannot be generated internally; and a separate layer keeps the EM skeleton (J, order-positioned, universally quantified in certification) apart from proof-theoretic witnesses (ℕ, existentially interpreted per skeleton interpretation). The finite-member consistency predicate lives over the expansion; the endpoint returns to L'[[J]] by the reduct lemma.

def FirstOrder.Language.henkinConst {L : Language} (n : ℕ) : (L.withConstants ℕ).Term Empty

The n-th Henkin witness constant of a constant expansion L[[ℕ]], as a closed term.

Equations

• FirstOrder.Language.henkinConst n = FirstOrder.Language.func (Sum.inr n) Fin.elim0

@[reducible, inline]

abbrev FirstOrder.Language.henkinConstsIn {L'' : Language} {J α : Type} {n : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) : Set ℕ

The Henkin-constant support of an expansion formula — the generalized sentenceJConsts at base L'[[J]] and constant type ℕ. Freshness of a witness index n for a fragment F is ∀ τ ∈ F, n ∉ henkinConstsIn τ.

Equations

• FirstOrder.Language.henkinConstsIn φ = FirstOrder.Language.sentenceJConsts φ

def FirstOrder.Language.expJConstsIn {L'' : Language} {J α : Type} {n : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) : Set J

The J-constant support of an expansion formula: the J-constants sit inside the base L''[[J]] layer, under Sum.inl ∘ Sum.inr.

Equations

• FirstOrder.Language.expJConstsIn φ = {j : J | ⟨0, Sum.inl (Sum.inr j)⟩ ∈ φ.functionsIn}

theorem FirstOrder.Language.Theoryω.model_reduct_of_expansion {L : Language} {γ : Type} (T : L.Theoryω) {N : Type} [(L.withConstants γ).Structure N] (h : ∀ τ ∈ T, Sentenceω.Realize (BoundedFormulaω.mapLanguage (L.lhomWithConstants γ) τ) N) : T.Model N

The forgetful/reduct lemma: realizing the mapLanguage-image of an L-theory in a constant-expansion structure yields, by reduct, a model of the original theory. The Henkin construction will model the expanded theory over (L'[[J]])[[ℕ]]; the Marker endpoint needs the L'[[J]] original.

theorem FirstOrder.Language.Theoryω.model_reduct_of_model_image {L : Language} {γ : Type} (T : L.Theoryω) {N : Type} [(L.withConstants γ).Structure N] (h : Model (BoundedFormulaω.mapLanguage (L.lhomWithConstants γ) '' T) N) : T.Model N

Image form of the reduct lemma: a model of the pushed-forward theory reducts to a model of the original.

Layer 4: the realizeWith evaluation API and the constant-agreement congruence

All structure instances are confined to the two wrapper definitions; every lemma statement mentions only the wrappers, so no local-instance synthesis ever leaks into downstream theorem statements. All later Marker closure rules are to be stated through this API.

def FirstOrder.Language.termValueWith {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {β : Type} (t : ((L''.withConstants J).withConstants ℕ).Term β) (v : β → M) : M

Evaluation of an expansion term under a skeleton interpretation σ : J → M and a Henkin interpretation h : ℕ → M.

Equations

• FirstOrder.Language.termValueWith σ h t v = FirstOrder.Language.Term.realize v t

def FirstOrder.Language.realizeWith {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) : Prop

Realization of an expansion formula under a skeleton interpretation σ : J → M and a Henkin interpretation h : ℕ → M.

Equations

• FirstOrder.Language.realizeWith σ h φ v xs = φ.Realize v xs

Constructor unfolds (term level)

@[simp]

theorem FirstOrder.Language.termValueWith_var {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {β : Type} (x : β) (v : β → M) : termValueWith σ h (var x) v = v x

@[simp]

theorem FirstOrder.Language.termValueWith_base {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {β : Type} {l : ℕ} (f : L''.Functions l) (ts : Fin l → ((L''.withConstants J).withConstants ℕ).Term β) (v : β → M) : termValueWith σ h (func (Sum.inl (Sum.inl f)) ts) v = Structure.funMap f fun (i : Fin l) => termValueWith σ h (ts i) v

@[simp]

theorem FirstOrder.Language.termValueWith_skeleton {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {β : Type} (j : J) (ts : Fin 0 → ((L''.withConstants J).withConstants ℕ).Term β) (v : β → M) : termValueWith σ h (func (Sum.inl (Sum.inr j)) ts) v = σ j

@[simp]

theorem FirstOrder.Language.termValueWith_henkin {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {β : Type} (m : ℕ) (ts : Fin 0 → ((L''.withConstants J).withConstants ℕ).Term β) (v : β → M) : termValueWith σ h (func (Sum.inr m) ts) v = h m

@[simp]

theorem FirstOrder.Language.termValueWith_henkinConst {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) (m : ℕ) (v : Empty → M) : termValueWith σ h (henkinConst m) v = h m

Constructor unfolds (formula level)

def FirstOrder.Language.baseRel {L'' : Language} {J : Type} {l : ℕ} : ((L''.withConstants J).withConstants ℕ).Relations l → L''.Relations l

The base relation symbol behind an expansion relation symbol (the constant layers add no relations).

Equations

• FirstOrder.Language.baseRel (Sum.inl (Sum.inl R)) = R
• FirstOrder.Language.baseRel (Sum.inl (Sum.inr e)) = Empty.elim e
• FirstOrder.Language.baseRel (Sum.inr e) = Empty.elim e

@[simp]

theorem FirstOrder.Language.realizeWith_falsum {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n : ℕ} (v : α → M) (xs : Fin n → M) : realizeWith σ h BoundedFormulaω.falsum v xs ↔ False

@[simp]

theorem FirstOrder.Language.realizeWith_equal {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n : ℕ} (t₁ t₂ : ((L''.withConstants J).withConstants ℕ).Term (α ⊕ Fin n)) (v : α → M) (xs : Fin n → M) : realizeWith σ h (BoundedFormulaω.equal t₁ t₂) v xs ↔ termValueWith σ h t₁ (Sum.elim v xs) = termValueWith σ h t₂ (Sum.elim v xs)

@[simp]

theorem FirstOrder.Language.realizeWith_rel {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n l : ℕ} (R : ((L''.withConstants J).withConstants ℕ).Relations l) (ts : Fin l → ((L''.withConstants J).withConstants ℕ).Term (α ⊕ Fin n)) (v : α → M) (xs : Fin n → M) : realizeWith σ h (BoundedFormulaω.rel R ts) v xs ↔ Structure.RelMap (baseRel R) fun (i : Fin l) => termValueWith σ h (ts i) (Sum.elim v xs)

@[simp]

theorem FirstOrder.Language.realizeWith_imp {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n : ℕ} (φ ψ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) : realizeWith σ h (φ.imp ψ) v xs ↔ realizeWith σ h φ v xs → realizeWith σ h ψ v xs

@[simp]

theorem FirstOrder.Language.realizeWith_all {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α (n + 1)) (v : α → M) (xs : Fin n → M) : realizeWith σ h φ.all v xs ↔ ∀ (x : M), realizeWith σ h φ v (Fin.snoc xs x)

@[simp]

theorem FirstOrder.Language.realizeWith_iSup {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n : ℕ} (φs : ℕ → ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) : realizeWith σ h (BoundedFormulaω.iSup φs) v xs ↔ ∃ (i : ℕ), realizeWith σ h (φs i) v xs

@[simp]

theorem FirstOrder.Language.realizeWith_iInf {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n : ℕ} (φs : ℕ → ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) : realizeWith σ h (BoundedFormulaω.iInf φs) v xs ↔ ∀ (i : ℕ), realizeWith σ h (φs i) v xs

@[simp]

theorem FirstOrder.Language.realizeWith_not {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) : realizeWith σ h φ.not v xs ↔ ¬realizeWith σ h φ v xs

@[simp]

theorem FirstOrder.Language.realizeWith_ex {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) {α : Type} {n : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α (n + 1)) (v : α → M) (xs : Fin n → M) : realizeWith σ h φ.ex v xs ↔ ∃ (x : M), realizeWith σ h φ v (Fin.snoc xs x)

theorem FirstOrder.Language.sentenceRealize_iff_realizeWith {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) (τ : ((L''.withConstants J).withConstants ℕ).Sentenceω) : τ.Realize M ↔ realizeWith σ h τ Empty.elim Fin.elim0

Bridge to the raw sentence satisfaction used by MarkerHenkinCert.

The constant-agreement congruence

theorem FirstOrder.Language.termValueWith_congr {L'' : Language} {J M : Type} [L''.Structure M] {σ σ' : J → M} {h h' : ℕ → M} {β : Type} (t : ((L''.withConstants J).withConstants ℕ).Term β) (hσ : ∀ (j : J), ⟨0, Sum.inl (Sum.inr j)⟩ ∈ t.functionsIn → σ j = σ' j) (hh : ∀ (m : ℕ), ⟨0, Sum.inr m⟩ ∈ t.functionsIn → h m = h' m) (v : β → M) : termValueWith σ h t v = termValueWith σ' h' t v

Term congruence: two skeleton interpretations agreeing on the occurring skeleton constants and two Henkin interpretations agreeing on the occurring witness constants give every term the same value.

theorem FirstOrder.Language.realizeWith_congr {L'' : Language} {J M : Type} [L''.Structure M] {σ σ' : J → M} {h h' : ℕ → M} {α : Type} {n : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (hσ : ∀ j ∈ expJConstsIn φ, σ j = σ' j) (hh : ∀ m ∈ henkinConstsIn φ, h m = h' m) (v : α → M) (xs : Fin n → M) : realizeWith σ h φ v xs ↔ realizeWith σ' h' φ v xs

Formula congruence — the semantic-support engine of the Marker construction: agreement on the occurring skeleton constants (expJConstsIn) and witness constants (henkinConstsIn) gives identical realization. This is what makes tuple-canonical colorings well-defined (C4 re-homogenization) and fresh witness indices harmless (C7).

Layer 5: the finite Henkin closure calculus

The freshness audit gate (settled by strengthening the predicate): henkinConstsIn is not automatically finite for an arbitrary Lω₁ω sentence — iSup/iInf can mention countably many witness constants (e.g. ⋁ₙ (dₙ = dₙ) has Henkin support all of ℕ) — so "pick a fresh witness index outside the fragment's Henkin support" needs an invariant. MarkerHenkinCert therefore carries a finite Henkin support H : Finset ℕ alongside the skeleton support S : Finset J. The invariant is self-maintaining and non-restrictive: the construction's seed sentences are mapLanguage-images of L'[[J]]-sentences (Henkin support ∅), and every closure operation shrinks the support (components, negations, implication branches) or grows it by finitely many constants (substitution instances) — an infinite-support sentence never enters a member of the Henkin enumeration.

Support lemmas for the expansion's skeleton constants

theorem FirstOrder.Language.expJConstsIn_not {L'' : Language} {J α : Type} {n : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) : expJConstsIn φ.not = expJConstsIn φ

Negation does not change the skeleton-constant support.

theorem FirstOrder.Language.expJConstsIn_component_iInf {L'' : Language} {J α : Type} {n : ℕ} (φs : ℕ → ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (k : ℕ) : expJConstsIn (φs k) ⊆ expJConstsIn (BoundedFormulaω.iInf φs)

A conjunction component's skeleton support is contained in the conjunction's.

theorem FirstOrder.Language.expJConstsIn_component_iSup {L'' : Language} {J α : Type} {n : ℕ} (φs : ℕ → ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (k : ℕ) : expJConstsIn (φs k) ⊆ expJConstsIn (BoundedFormulaω.iSup φs)

A disjunction component's skeleton support is contained in the disjunction's.

theorem FirstOrder.Language.expJConstsIn_imp_left {L'' : Language} {J α : Type} {n : ℕ} (φ ψ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) : expJConstsIn φ ⊆ expJConstsIn (φ.imp ψ)

An implication's antecedent skeleton support is contained in the implication's.

theorem FirstOrder.Language.expJConstsIn_imp_right {L'' : Language} {J α : Type} {n : ℕ} (φ ψ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) : expJConstsIn ψ ⊆ expJConstsIn (φ.imp ψ)

An implication's consequent skeleton support is contained in the implication's.

Support lemmas for the expansion's Henkin constants (wrappers around the generic

sentenceJConsts family, restated so rw matches the henkinConstsIn spelling)

theorem FirstOrder.Language.henkinConstsIn_not {L'' : Language} {J α : Type} {n : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) : henkinConstsIn φ.not = henkinConstsIn φ

theorem FirstOrder.Language.henkinConstsIn_component_iInf {L'' : Language} {J α : Type} {n : ℕ} (φs : ℕ → ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (k : ℕ) : henkinConstsIn (φs k) ⊆ henkinConstsIn (BoundedFormulaω.iInf φs)

theorem FirstOrder.Language.henkinConstsIn_component_iSup {L'' : Language} {J α : Type} {n : ℕ} (φs : ℕ → ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) (k : ℕ) : henkinConstsIn (φs k) ⊆ henkinConstsIn (BoundedFormulaω.iSup φs)

theorem FirstOrder.Language.henkinConstsIn_imp_left {L'' : Language} {J α : Type} {n : ℕ} (φ ψ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) : henkinConstsIn φ ⊆ henkinConstsIn (φ.imp ψ)

theorem FirstOrder.Language.henkinConstsIn_imp_right {L'' : Language} {J α : Type} {n : ℕ} (φ ψ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α n) : henkinConstsIn ψ ⊆ henkinConstsIn (φ.imp ψ)

The finite-member predicates

def FirstOrder.Language.MarkerHenkinBody {L'' : Language} {J : Type} [LinearOrder J] (M : Type) [L''.Structure M] [LinearOrder M] (α : Ordinal.{0}) (S : Finset J) (F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω) : Prop

The certificate body at an explicit skeleton support S: a (ℶ_α)⁺-suborder e of the source, and — for EVERY skeleton interpretation increasing on S into e's range — SOME Henkin interpretation making every member true. The skeleton side stays universal (the EM tuples); the witness side is existential per interpretation, because quantifier witnesses vary with the tuple. The support-tracking conjuncts live in the wrapping predicates.

Equations

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

def FirstOrder.Language.MarkerHenkinCert {L'' : Language} {J : Type} [LinearOrder J] (M : Type) [L''.Structure M] [LinearOrder M] (α : Ordinal.{0}) (F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω) : Prop

The per-level Henkin–Marker certification of a finite fragment over the expansion (L''[[J]])[[ℕ]]: a finite skeleton support S, a finite Henkin support H (the freshness invariant), and a body at S.

Equations

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

def FirstOrder.Language.MarkerHenkinConsistent {L'' : Language} {J : Type} [LinearOrder J] (M : Type) [L''.Structure M] [LinearOrder M] (F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω) : Prop

The finite-member consistency predicate: a UNIFORM finite support (S, H) (fixed across all levels — this is what the re-homogenization room lemma needs, and what the base case markerStage_homogeneous naturally provides) together with certification bodies at cofinally many levels below ω₁. The arbitrary-set extension field and the global C4 uniformization of the ambient ConsistencyPropertyEq API are deliberately avoided: the Henkin construction consumes finite members along its enumeration, choosing disjuncts and witnesses per member (the classical Marker/Keisler shape).

Equations

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

theorem FirstOrder.Language.MarkerHenkinBody.mono {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α : Ordinal.{0}} {S : Finset J} {F F' : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hFF : F' ⊆ F) (hb : MarkerHenkinBody M α S F) : MarkerHenkinBody M α S F'

The body is monotone (downward-closed) in the fragment, at fixed support.

theorem FirstOrder.Language.MarkerHenkinBody.insert_of_semantic {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α : Ordinal.{0}} {S : Finset J} {F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hb : MarkerHenkinBody M α S F) {trigger new : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : trigger ∈ F) (hder : ∀ (σ : J → M) (h : ℕ → M), realizeWith σ h trigger Empty.elim Fin.elim0 → realizeWith σ h new Empty.elim Fin.elim0) : MarkerHenkinBody M α S (insert new F)

Body-level semantic insertion: if a trigger member semantically entails a new sentence under every interpretation pair, adjoining new preserves the body (same suborder, same witnesses).

theorem FirstOrder.Language.MarkerHenkinCert.mono {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α : Ordinal.{0}} {F F' : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hFF : F' ⊆ F) (hc : MarkerHenkinCert M α F) : MarkerHenkinCert M α F'

Certification is monotone (downward-closed) in the fragment.

theorem FirstOrder.Language.MarkerHenkinConsistent.mono {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F F' : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (hFF : F' ⊆ F) (h : MarkerHenkinConsistent M F) : MarkerHenkinConsistent M F'

Finite-member consistency is monotone (downward-closed).

theorem FirstOrder.Language.MarkerHenkinCert.insert_of_semantic {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α : Ordinal.{0}} {F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hc : MarkerHenkinCert M α F) {trigger new : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : trigger ∈ F) (hJ : expJConstsIn new ⊆ expJConstsIn trigger) (hN : henkinConstsIn new ⊆ henkinConstsIn trigger) (hder : ∀ (σ : J → M) (h : ℕ → M), realizeWith σ h trigger Empty.elim Fin.elim0 → realizeWith σ h new Empty.elim Fin.elim0) : MarkerHenkinCert M α (insert new F)

The semantic insertion scheme behind the choice-free closure rules: if a trigger member semantically entails a new sentence under every interpretation pair, and neither constant support grows, then adjoining new preserves certification — same supports, same suborder, same witnesses.

theorem FirstOrder.Language.MarkerHenkinCert.falsum_notMem {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α : Ordinal.{0}} {F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hc : MarkerHenkinCert M α F) : BoundedFormulaω.falsum ∉ F

C0 (no falsum): a certified fragment cannot contain ⊥.

theorem FirstOrder.Language.MarkerHenkinCert.not_mem_and_not_mem {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α : Ordinal.{0}} {F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hc : MarkerHenkinCert M α F) (τ : ((L''.withConstants J).withConstants ℕ).Sentenceω) : ¬(τ ∈ F ∧ BoundedFormulaω.not τ ∈ F)

C0 (no contradiction): a certified fragment cannot contain both a sentence and its negation.

theorem FirstOrder.Language.MarkerHenkinConsistent.insert_of_semantic {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {trigger new : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : trigger ∈ F) (hJ : expJConstsIn new ⊆ expJConstsIn trigger) (hN : henkinConstsIn new ⊆ henkinConstsIn trigger) (hder : ∀ (σ : J → M) (hk : ℕ → M), realizeWith σ hk trigger Empty.elim Fin.elim0 → realizeWith σ hk new Empty.elim Fin.elim0) : MarkerHenkinConsistent M (insert new F)

The finite-member insertion scheme at the consistency level (uniform support preserved).

theorem FirstOrder.Language.MarkerHenkinConsistent.not_not {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {φ : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.not φ).not ∈ F) : MarkerHenkinConsistent M (insert φ F)

C2 (double negation): ¬¬φ ∈ F allows adjoining φ.

theorem FirstOrder.Language.MarkerHenkinConsistent.iInf_component {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {φs : ℕ → ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.iInf φs ∈ F) (k : ℕ) : MarkerHenkinConsistent M (insert (φs k) F)

C3 (conjunction components): ⋀ᵢ φᵢ ∈ F allows adjoining every component.

theorem FirstOrder.Language.MarkerHenkinConsistent.neg_iSup_component {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {φs : ℕ → ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.iSup φs).not ∈ F) (k : ℕ) : MarkerHenkinConsistent M (insert (BoundedFormulaω.not (φs k)) F)

C4' (negated-disjunction components): ¬⋁ᵢ φᵢ ∈ F allows adjoining every negated component.

theorem FirstOrder.Language.MarkerHenkinConsistent.neg_imp_left {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {φ ψ : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.imp φ ψ).not ∈ F) : MarkerHenkinConsistent M (insert φ F)

C1' (negated implication, antecedent): ¬(φ → ψ) ∈ F allows adjoining φ.

theorem FirstOrder.Language.MarkerHenkinConsistent.neg_imp_right {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {φ ψ : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.imp φ ψ).not ∈ F) : MarkerHenkinConsistent M (insert (BoundedFormulaω.not ψ) F)

C1' (negated implication, consequent): ¬(φ → ψ) ∈ F allows adjoining ¬ψ.

Layer 5b engine: re-homogenization

The reusable machinery for the branch/index choice rules (C1, C3', C4): color the support tuples of a high-level certificate body by the branch a realizing interpretation selects, re-homogenize inside the existing suborder via finiteArityHomogeneousUpTo_beth_stage at a level lower by the finite ladder cost 2·|S|+2, and read off a uniform branch.

noncomputable def FirstOrder.Language.tupleInterp {J : Type} [LinearOrder J] {M : Type} [LinearOrder M] {D : Type} [LinearOrder D] (S : Finset J) (e : D ↪o M) (t : Fin S.card → D) (dflt : M) : J → M

The skeleton interpretation determined by a source tuple t : Fin S.card → D and a suborder e : D ↪o M: the i-th element of S maps to e (t i), off S to a default.

Equations

• FirstOrder.Language.tupleInterp S e t dflt j = if h : j ∈ S then e (t ((S.orderIsoOfFin ⋯).symm ⟨j, h⟩)) else dflt

theorem FirstOrder.Language.tupleInterp_orderEmbOfFin {J : Type} [LinearOrder J] {M : Type} [LinearOrder M] {D : Type} [LinearOrder D] (S : Finset J) (e : D ↪o M) (t : Fin S.card → D) (dflt : M) (i : Fin S.card) : tupleInterp S e t dflt ((S.orderEmbOfFin ⋯) i) = e (t i)

theorem FirstOrder.Language.strictMonoOn_tupleInterp {J : Type} [LinearOrder J] {M : Type} [LinearOrder M] {D : Type} [LinearOrder D] (S : Finset J) (e : D ↪o M) {t : Fin S.card → D} (ht : StrictMono t) (dflt : M) : StrictMonoOn (tupleInterp S e t dflt) ↑S

theorem FirstOrder.Language.tupleInterp_mem_range {J : Type} [LinearOrder J] {M : Type} [LinearOrder M] {D : Type} [LinearOrder D] (S : Finset J) (e : D ↪o M) (t : Fin S.card → D) (dflt : M) (j : J) : j ∈ S → tupleInterp S e t dflt j ∈ Set.range ⇑e

theorem FirstOrder.Language.tupleInterp_eqOn {J : Type} [LinearOrder J] {M : Type} [LinearOrder M] {D : Type} [LinearOrder D] (S : Finset J) (e : D ↪o M) (t : Fin S.card → D) (dflt : M) {σ : J → M} (h : ∀ (i : Fin S.card), e (t i) = σ ((S.orderEmbOfFin ⋯) i)) (j : J) : j ∈ S → tupleInterp S e t dflt j = σ j

On the support, tupleInterp agrees with any σ matching it index-by-index.

theorem FirstOrder.Language.exists_orderEmb_fin {D : Type} [LinearOrder D] [Infinite D] (m : ℕ) : Nonempty (Fin m ↪o D)

A finite tuple order-embedding into any infinite linear order exists.

theorem FirstOrder.Language.exists_factor_tuple {J : Type} [LinearOrder J] {M : Type} [LinearOrder M] {D₀ D : Type} [LinearOrder D₀] [LinearOrder D] (S : Finset J) (e : D ↪o M) (e' : D₀ ↪o D) {σ : J → M} (hmono : StrictMonoOn σ ↑S) (hrange : ∀ j ∈ S, σ j ∈ Set.range ⇑(RelEmbedding.trans e' e)) : ∃ (t : Fin S.card → D), StrictMono t ∧ (∀ (i : Fin S.card), t i ∈ Set.range ⇑e') ∧ ∀ (i : Fin S.card), e (t i) = σ ((S.orderEmbOfFin ⋯) i)

Support-tuple factoring: an admissible σ for the composite suborder e'.trans e factors through the support into a source tuple t landing in Set.range e' and matching σ on S index-by-index.

theorem FirstOrder.Language.MarkerHenkinBody.branch_choice {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α₀ α : Ordinal.{0}} {S : Finset J} {F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hroom : α₀ + ↑(2 * S.card + 2) ≤ α) (hb : MarkerHenkinBody M α S F) (hFsupp : ∀ τ ∈ F, expJConstsIn τ ⊆ ↑S) {K : Type} [Countable K] (branch : K → ((L''.withConstants J).withConstants ℕ).Sentenceω) (hbranchSupp : ∀ (k : K), expJConstsIn (branch k) ⊆ ↑S) (hcover : ∀ (σ : J → M) (h : ℕ → M), (∀ τ ∈ F, realizeWith σ h τ Empty.elim Fin.elim0) → ∃ (k : K), realizeWith σ h (branch k) Empty.elim Fin.elim0) : ∃ (k : K), MarkerHenkinBody M α₀ S (insert (branch k) F)

The re-homogenization engine. From a certificate body of F at a level α exceeding the target α₀ by the finite ladder cost 2·|S|+2, a covering branch family whose members have skeleton support inside S, produce ONE branch k and a body of insert (branch k) F at the target level α₀. The branch is uniform on the support tuples of the output suborder (read off finiteArityHomogeneousUpTo_beth_stage); every admissible interpretation of the output suborder factors through a support tuple, whose realizing interpretation selects branch k, and constant-agreement congruence transfers realization back.

Layer 5b-2: the branch/index choice rules

theorem FirstOrder.Language.MarkerHenkinConsistent.branch_choice {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {K : Type} [Countable K] (branch : K → ((L''.withConstants J).withConstants ℕ).Sentenceω) {trigger : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : trigger ∈ F) (hbJ : ∀ (k : K), expJConstsIn (branch k) ⊆ expJConstsIn trigger) (hbN : ∀ (k : K), henkinConstsIn (branch k) ⊆ henkinConstsIn trigger) (hcover : ∀ (σ : J → M) (hk : ℕ → M), realizeWith σ hk trigger Empty.elim Fin.elim0 → ∃ (k : K), realizeWith σ hk (branch k) Empty.elim Fin.elim0) : ∃ (k : K), MarkerHenkinConsistent M (insert (branch k) F)

Consistency-level branch choice (re-homogenization + the ω₁-pigeonhole assembly): a covering branch family for a trigger ∈ F, whose members' constant supports lie inside the trigger's, yields ONE branch k with insert (branch k) F consistent. Per target level the body comes from MarkerHenkinBody.branch_choice (asked at the ladder-cost-offset level, kept below ω₁ by add_natCast_lt_omega_one); the single uniform k comes from exists_uniform_of_cofinal_countable (ω₁ is regular). Uniform support (S, H) is preserved.

theorem FirstOrder.Language.MarkerHenkinConsistent.iSup_choice {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {φs : ℕ → ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.iSup φs ∈ F) : ∃ (k : ℕ), MarkerHenkinConsistent M (insert (φs k) F)

C4 (disjunction witness): ⋁ᵢ φᵢ ∈ F yields a uniform disjunct k with insert (φs k) F consistent.

theorem FirstOrder.Language.MarkerHenkinConsistent.neg_iInf_choice {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {φs : ℕ → ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : (BoundedFormulaω.iInf φs).not ∈ F) : ∃ (k : ℕ), MarkerHenkinConsistent M (insert (BoundedFormulaω.not (φs k)) F)

C3' (negated-conjunction witness): ¬⋀ᵢ φᵢ ∈ F yields a uniform index k with insert (φs k).not F consistent.

theorem FirstOrder.Language.MarkerHenkinConsistent.imp_choice {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {φ ψ : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hmem : BoundedFormulaω.imp φ ψ ∈ F) : MarkerHenkinConsistent M (insert (BoundedFormulaω.not φ) F) ∨ MarkerHenkinConsistent M (insert ψ F)

C1 (implication): φ → ψ ∈ F — one of insert φ.not F, insert ψ F is consistent (the branch is chosen uniformly over the support tuples).

Layer 5c: the Henkin witness rule (C7)

The one closure rule of a different shape: no re-homogenization, but a fresh Henkin constant. From ∃x φ(x) ∈ F, pick a witness index n outside the finite Henkin support H, update the Henkin interpretation at n to the existential witness (per skeleton interpretation), and adjoin the instance φ(dₙ). The finite-support invariant is what makes "fresh n" available.

noncomputable def FirstOrder.Language.witnessSentence {L'' : Language} {J : Type} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω Empty 1) (n : ℕ) : ((L''.withConstants J).withConstants ℕ).Sentenceω

The Henkin witness instance of an existential: φ with its last bound variable filled by the n-th Henkin constant.

Equations

• FirstOrder.Language.witnessSentence φ n = FirstOrder.Language.BoundedFormulaω.subst φ.openBounds fun (x : Fin 1) => FirstOrder.Language.henkinConst n

theorem FirstOrder.Language.functionsIn_ex {L'' : Language} {J α : Type} {m : ℕ} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω α (m + 1)) : φ.ex.functionsIn = φ.functionsIn

∃ does not change the mentioned function symbols.

theorem FirstOrder.Language.expJConstsIn_ex {L'' : Language} {J : Type} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω Empty 1) : expJConstsIn φ.ex = expJConstsIn φ

theorem FirstOrder.Language.henkinConstsIn_ex {L'' : Language} {J : Type} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω Empty 1) : henkinConstsIn φ.ex = henkinConstsIn φ

theorem FirstOrder.Language.functionsIn_henkinConst {L'' : Language} {J : Type} (n : ℕ) : (henkinConst n).functionsIn ⊆ {⟨0, Sum.inr n⟩}

The witness constant dₙ's only mentioned symbol is the n-th Henkin constant.

theorem FirstOrder.Language.functionsIn_witnessSentence {L'' : Language} {J : Type} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω Empty 1) (n : ℕ) : BoundedFormulaω.functionsIn (witnessSentence φ n) ⊆ φ.functionsIn ∪ {⟨0, Sum.inr n⟩}

The witness sentence adds no new function symbol beyond φ's and the fresh constant dₙ.

theorem FirstOrder.Language.expJConstsIn_witnessSentence {L'' : Language} {J : Type} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω Empty 1) (n : ℕ) : expJConstsIn (witnessSentence φ n) ⊆ expJConstsIn φ

theorem FirstOrder.Language.henkinConstsIn_witnessSentence {L'' : Language} {J : Type} (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω Empty 1) (n : ℕ) : henkinConstsIn (witnessSentence φ n) ⊆ insert n (henkinConstsIn φ)

theorem FirstOrder.Language.realizeWith_witness {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (h : ℕ → M) (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω Empty 1) (n : ℕ) : realizeWith σ h (witnessSentence φ n) Empty.elim Fin.elim0 ↔ realizeWith σ h φ Empty.elim (Fin.snoc Fin.elim0 (h n))

The semantic bridge: realizing the witness sentence is realizing φ with the last bound variable set to the Henkin interpretation of dₙ.

theorem FirstOrder.Language.MarkerHenkinBody.witness {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α : Ordinal.{0}} {S : Finset J} {F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hb : MarkerHenkinBody M α S F) {φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω Empty 1} (hmem : φ.ex ∈ F) (n : ℕ) (hn : ∀ τ ∈ F, n ∉ henkinConstsIn τ) : MarkerHenkinBody M α S (insert (witnessSentence φ n) F)

Body-level C7: from ∃x φ(x) ∈ F and a Henkin index n fresh for F, the witness instance can be adjoined — update the Henkin interpretation at n to the existential witness; n's freshness leaves every old member unchanged (realizeWith_congr).

theorem FirstOrder.Language.MarkerHenkinConsistent.ex_witness {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) {φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω Empty 1} (hmem : φ.ex ∈ F) : ∃ (n : ℕ), MarkerHenkinConsistent M (insert (witnessSentence φ n) F)

C7 (existential witness): ∃x φ(x) ∈ F yields a fresh Henkin index n with insert (witnessSentence φ n) F consistent — the new Henkin support is insert n H.

Layer 6a: the finite-support universe and the restricted extension rule

The bespoke finite-Henkin adapter avoids the ambient ConsistencyPropertyEq (whose extension field quantifies over ARBITRARY sentences, which Marker consistency cannot supply at infinite constant-support). Instead it works over the sentences of finite constant support — exactly the sentences the Marker recursion from the template seed ever produces — and replaces the arbitrary-sentence extension field with a restricted extension rule proved by the same Layer-5b re-homogenization engine (branch over Bool, colour support tuples by whether τ is realized).

def FirstOrder.Language.HasFiniteConstSupport {L'' : Language} {J : Type} (τ : ((L''.withConstants J).withConstants ℕ).Sentenceω) : Prop

A sentence of finite constant support: finitely many J-constants and finitely many Henkin constants. The restricted universe the adapter decides over.

Equations

• FirstOrder.Language.HasFiniteConstSupport τ = ∃ (S : Finset J) (H : Finset ℕ), FirstOrder.Language.expJConstsIn τ ⊆ ↑S ∧ FirstOrder.Language.henkinConstsIn τ ⊆ ↑H

@[reducible, inline]

abbrev FirstOrder.Language.FSentence {L'' : Language} {J : Type} : Type

The subtype of finite-constant-support sentences — the universe of the maximal finite-support theory.

Equations

• FirstOrder.Language.FSentence = { τ : ((L''.withConstants J).withConstants ℕ).Sentenceω // FirstOrder.Language.HasFiniteConstSupport τ }

theorem FirstOrder.Language.HasFiniteConstSupport.not {L'' : Language} {J : Type} {τ : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hτ : HasFiniteConstSupport τ) : HasFiniteConstSupport (BoundedFormulaω.not τ)

Negation preserves finite constant support.

theorem FirstOrder.Language.MarkerHenkinBody.enlarge_support {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α : Ordinal.{0}} {S S' : Finset J} {F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hSS : S ⊆ S') (hb : MarkerHenkinBody M α S F) : MarkerHenkinBody M α S' F

A body over S is a body over any larger support (fewer admissible interpretations).

theorem FirstOrder.Language.MarkerHenkinConsistent.extension {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) (τ : ((L''.withConstants J).withConstants ℕ).Sentenceω) (hτ : HasFiniteConstSupport τ) : MarkerHenkinConsistent M (insert τ F) ∨ MarkerHenkinConsistent M (insert (BoundedFormulaω.not τ) F)

The restricted extension rule (the replacement for the ambient extension field): any finite-constant-support sentence τ can be decided — one of insert τ F, insert τ.not F is Marker-consistent. Enlarge the uniform support by τ's finite supports, re-homogenize the Boolean "is τ realized" colouring of the support tuples (MarkerHenkinBody.branch_choice, covering is the unconditional tautology τ ∨ ¬τ), and uniformize the branch over the cofinal α-schedule.

Layer 6b: the equality closure rules (C5/C6)

The equality rules the term-model quotient and truth lemma will need on the restricted maximal theory. Both are proved semantically (certification is realizability in M, whose equality is genuine) via unconditional/entailed insertion, with finite constant support tracked through the syntactic support API.

theorem FirstOrder.Language.HasFiniteConstSupport_of_functionsIn_finite {L'' : Language} {J : Type} {τ : ((L''.withConstants J).withConstants ℕ).Sentenceω} (hfin : (BoundedFormulaω.functionsIn τ).Finite) : HasFiniteConstSupport τ

A sentence mentioning only finitely many function symbols has finite constant support: expJConstsIn/henkinConstsIn are preimages of functionsIn under injective maps.

theorem FirstOrder.Language.MarkerHenkinBody.insert_of_entailed {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {α : Ordinal.{0}} {S : Finset J} {F : Set ((L''.withConstants J).withConstants ℕ).Sentenceω} (hb : MarkerHenkinBody M α S F) (new : ((L''.withConstants J).withConstants ℕ).Sentenceω) (hent : ∀ (σ : J → M) (hk : ℕ → M), (∀ ρ ∈ F, realizeWith σ hk ρ Empty.elim Fin.elim0) → realizeWith σ hk new Empty.elim Fin.elim0) : MarkerHenkinBody M α S (insert new F)

Body-level entailed insertion: if the members of F semantically entail new under every interpretation, adjoining new preserves the body (same suborder, same witnesses).

theorem FirstOrder.Language.MarkerHenkinConsistent.insert_entailed {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) (new : ((L''.withConstants J).withConstants ℕ).Sentenceω) (hnew : HasFiniteConstSupport new) (hent : ∀ (σ : J → M) (hk : ℕ → M), (∀ ρ ∈ ↑F, realizeWith σ hk ρ Empty.elim Fin.elim0) → realizeWith σ hk new Empty.elim Fin.elim0) : MarkerHenkinConsistent M (insert new F)

Consistency-level entailed insertion: a finite-support sentence entailed by F (under every interpretation) can be adjoined; the uniform support grows by the new sentence's finite supports. No re-homogenization (the entailment is unconditional over the branch).

theorem FirstOrder.Language.MarkerHenkinConsistent.eq_refl {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) (t : ((L''.withConstants J).withConstants ℕ).Term (Empty ⊕ Fin 0)) : MarkerHenkinConsistent M (insert (BoundedFormulaω.equal t t) F)

C5 (equality reflexivity): t = t can always be adjoined — it is valid, so any realizing interpretation realizes it too.

theorem FirstOrder.Language.functionsIn_eq_subst_subset {L'' : Language} {J : Type} (t₁ t₂ : ((L''.withConstants J).withConstants ℕ).Term Empty) (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω (Fin 1) 0) : (φ.subst fun (x : Fin 1) => t₂).functionsIn ⊆ (φ.subst fun (x : Fin 1) => t₁).functionsIn ∪ (BoundedFormulaω.equal (Term.relabel Sum.inl t₁) (Term.relabel Sum.inl t₂)).functionsIn

The C6 substitution instance mentions no symbol beyond the old instance φ(t₁) and the equality sentence — the syntactic support bound behind eq_subst's finite support.

theorem FirstOrder.Language.termValueWith_relabel_inl {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (hk : ℕ → M) (t : ((L''.withConstants J).withConstants ℕ).Term Empty) : termValueWith σ hk (Term.relabel Sum.inl t) (Sum.elim Empty.elim Fin.elim0) = termValueWith σ hk t Empty.elim

Realizing a relabel of a closed term is realizing the term (the extra bound slot is vacuous).

theorem FirstOrder.Language.realizeWith_subst_const {L'' : Language} {J M : Type} [L''.Structure M] (σ : J → M) (hk : ℕ → M) (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω (Fin 1) 0) (t : ((L''.withConstants J).withConstants ℕ).Term Empty) : realizeWith σ hk (φ.subst fun (x : Fin 1) => t) Empty.elim Fin.elim0 ↔ realizeWith σ hk φ (fun (x : Fin 1) => termValueWith σ hk t Empty.elim) Fin.elim0

The substitution-of-a-closed-term bridge: realizing φ(t) is realizing φ with its bound variable set to the value of t.

theorem FirstOrder.Language.MarkerHenkinConsistent.eq_subst {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {F : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω} (h : MarkerHenkinConsistent M F) (t₁ t₂ : ((L''.withConstants J).withConstants ℕ).Term Empty) (φ : ((L''.withConstants J).withConstants ℕ).BoundedFormulaω (Fin 1) 0) (hmem_eq : BoundedFormulaω.equal (Term.relabel Sum.inl t₁) (Term.relabel Sum.inl t₂) ∈ F) (hmem_φ : (φ.subst fun (x : Fin 1) => t₁) ∈ F) : MarkerHenkinConsistent M (insert (φ.subst fun (x : Fin 1) => t₂) F)

C6 (equality substitution): from t₁ = t₂ ∈ F and φ(t₁) ∈ F, the instance φ(t₂) can be adjoined — the equality forces equal term values, and realizeWith_subst_const transports φ. The support of φ(t₂) stays inside F's uniform support (functionsIn_eq_subst_subset).

Layer 6c: the maximal finite-support theory (Zorn)

The finite closure calculus (C0–C7) is turned into a complete theory over the finite-support universe by a finite-character Zorn argument, mirroring ConsistencyProperty.chain_closure but with completeness only for finite-support sentences — exactly what the restricted truth lemma will need. Parameterized by a consistent seed (the base consistency hook is a separate cross-file integration; the abstract machinery here fixes the shape it must feed).

def FirstOrder.Language.FSentence.not {L'' : Language} {J : Type} (τ : FSentence) : FSentence

Negation on the finite-support universe.

Equations

• τ.not = ⟨FirstOrder.Language.BoundedFormulaω.not ↑τ, ⋯⟩

def FirstOrder.Language.MarkerConsistentFamily {L'' : Language} {J : Type} [LinearOrder J] (M : Type) [L''.Structure M] [LinearOrder M] (X : Set FSentence) : Prop

Finite-character Marker consistency of a set of finite-support sentences: every finite subset is Marker–Henkin consistent. This is the family Zorn runs over.

Equations

• FirstOrder.Language.MarkerConsistentFamily M X = ∀ (F : Finset FirstOrder.Language.FSentence), ↑F ⊆ X → FirstOrder.Language.MarkerHenkinConsistent M (Finset.image Subtype.val F)

theorem FirstOrder.Language.MarkerConsistentFamily.mono {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {X X' : Set FSentence} (hXX : X' ⊆ X) (h : MarkerConsistentFamily M X) : MarkerConsistentFamily M X'

Finite-character consistency is downward-closed in the set.

theorem FirstOrder.Language.MarkerConsistentFamily.sUnion_chain {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {𝒞 : Set (Set FSentence)} (h𝒞 : ∀ Y ∈ 𝒞, MarkerConsistentFamily M Y) (hchain : IsChain (fun (x1 x2 : Set FSentence) => x1 ⊆ x2) 𝒞) (hne : 𝒞.Nonempty) : MarkerConsistentFamily M (⋃₀ 𝒞)

Chain closure: the union of a nonempty ⊆-chain of finite-character-consistent sets is finite-character consistent — a finite subset of the union lies in one chain member.

theorem FirstOrder.Language.exists_maximal_markerConsistent {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] (X₀ : Set FSentence) (hX₀ : MarkerConsistentFamily M X₀) : ∃ (m : Set FSentence), X₀ ⊆ m ∧ Maximal (MarkerConsistentFamily M) m

The maximal finite-support theory: any finite-character-consistent seed extends to a maximal one (Zorn, chain closure supplying the upper bounds).

Membership calculus of the maximal theory

theorem FirstOrder.Language.not_mem_of_maximal {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {m : Set FSentence} (hmax : Maximal (MarkerConsistentFamily M) m) {τ : FSentence} (hτ : τ ∉ m) : ∃ (F : Finset FSentence), ↑F ⊆ m ∧ ¬MarkerHenkinConsistent M (insert (↑τ) (Finset.image Subtype.val F))

A sentence outside a maximal theory is refuted by some finite fragment: adjoining it to that fragment breaks consistency.

theorem FirstOrder.Language.MarkerConsistentFamily.mem_or_not_mem {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {m : Set FSentence} (hmax : Maximal (MarkerConsistentFamily M) m) (τ : FSentence) : τ ∈ m ∨ τ.not ∈ m

Restricted completeness: a maximal finite-support theory decides every finite-support sentence. From maximality, insert τ m and insert τ.not m are both inconsistent as families when τ, τ.not ∉ m; combining the two refuting fragments and applying the extension rule yields a contradiction.

theorem FirstOrder.Language.MarkerConsistentFamily.mem_of_insert_consistent {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {m : Set FSentence} (hmax : Maximal (MarkerConsistentFamily M) m) (new : FSentence) (hins : ∀ (F : Finset FSentence), ↑F ⊆ m → MarkerHenkinConsistent M (insert (↑new) (Finset.image Subtype.val F))) : new ∈ m

The membership-insertion principle for the maximal theory: a finite-support sentence whose adjunction to every fragment of m stays consistent is a member of m. This turns each fragment-level closure rule into a membership rule.

theorem FirstOrder.Language.MarkerConsistentFamily.mem_of_trigger {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {m : Set FSentence} (hmax : Maximal (MarkerConsistentFamily M) m) {trigger : FSentence} (htrig : trigger ∈ m) (new : FSentence) (rule : ∀ (G : Finset ((L''.withConstants J).withConstants ℕ).Sentenceω), ↑trigger ∈ G → MarkerHenkinConsistent M G → MarkerHenkinConsistent M (insert (↑new) G)) : new ∈ m

The membership-closure engine: a fragment-level closure rule (adjoining new to any consistent fragment containing the trigger stays consistent) lifts, given trigger ∈ m, to new ∈ m. Every named closure membership rule below is a one-line instance.

theorem FirstOrder.Language.MarkerConsistentFamily.mem_not_not {L'' : Language} {J : Type} [LinearOrder J] {M : Type} [L''.Structure M] [LinearOrder M] {m : Set FSentence} (hmax : Maximal (MarkerConsistentFamily M) m) {φ : FSentence} (hmem : φ.not.not ∈ m) : φ ∈ m

C2 in membership form: ¬¬φ ∈ m implies φ ∈ m.