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

The ω₁-pigeonhole engine and the stated uniformization test

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}

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_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

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_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

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

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

sentenceJConsts family, restated so rw matches the henkinConstsIn spelling)

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

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.

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

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

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

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.

Membership calculus of the maximal theory