The closure fields (issue #12, commit 4b part 3 — Exercise 4.28)

The fifteen closure rules of the well-ordering consistency property, as WOMem-preservation theorems, in the reviewed order: C0 and deterministic connectives; branching through the cofinal-fiber lemma; equality/relation congruence; constant-sensitive rules through the range split and mark_rat; the fresh odd witness (whose index is chosen separately to avoid the finite remainder support — parity only places it outside the rational range).

Every rule opens with the ∈ Bφ split (WOMem.union_of_mem_base: adding a base member changes nothing); the genuine extensions go through WOMem.extend, whose three obligations (universe, finite support, and (*) at every level) are discharged per-rule from the GenU reachability lemmas, the sentenceJConsts monotonicity calculus, and the StarWitness operations of the previous commits.

The split and extension steps

theorem FirstOrder.Language.WOMem.union_of_mem_base {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) {χ : (L.withConstants ℕ).Sentenceω} (hχ : χ ∈ baseDiagram φ lt) : WOMem φ lt (S ∪ {χ})

Adding a base member changes nothing.

theorem FirstOrder.Language.WOMem.extend {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) {χ : (L.withConstants ℕ).Sentenceω} (hχnb : χ ∉ baseDiagram φ lt) (hχU : χ ∈ GenU (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ)) (hχsupp : (sentenceJConsts χ).Finite) (hstar : ∀ α < (Cardinal.aleph 1).ord, StarCondition φ lt (S \ baseDiagram φ lt ∪ {χ}) α) : WOMem φ lt (S ∪ {χ})

The generic extension step: adding a non-base sentence to a member preserves membership, given the universe, finite-support, and (*) obligations.

theorem FirstOrder.Language.WOMem.jConsts_finite_of_mem {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) {χ : (L.withConstants ℕ).Sentenceω} (hχ : χ ∈ S) : (sentenceJConsts χ).Finite

The support of any member sentence is finite (base: the lift is constant-free, atoms have two constants; remainder: the member's finite-support field).

theorem FirstOrder.Language.StarWitness.realize_source {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} {α : Ordinal.{0}} (W : StarWitness φ lt Γ α) {χ : (L.withConstants ℕ).Sentenceω} (hχ : χ ∈ Γ ∨ χ = BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) : χ.Realize W.M

A remainder-or-root sentence is realized by every star witness.

theorem FirstOrder.Language.StarWitness.hsupp_of_subset {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} {α : Ordinal.{0}} (W : StarWitness φ lt Γ α) {χ ψ : (L.withConstants ℕ).Sentenceω} (hψ : ψ ∈ Γ) (hsub : sentenceJConsts χ ⊆ sentenceJConsts ψ) (q : ℚ) : ratConstIdx q ∈ sentenceJConsts χ → q ∈ Set.range W.mark

Rationals mentioned by a sentence with support inside a remainder member's support are marked.

theorem FirstOrder.Language.WOMem.mem_cases {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} : WOMem φ lt S → ∀ {χ : (L.withConstants ℕ).Sentenceω} (hχ : χ ∈ S), χ ∈ S \ baseDiagram φ lt ∨ χ = BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ ∨ ∃ (q : ℚ) (r : ℚ), q < r ∧ χ = ratLtAtom lt q r

Locating a member of S for the (*) argument: it lies in the remainder, or it is the lifted root, or it is a positive diagram atom.

theorem FirstOrder.Language.one_lt_omega1 : 1 < (Cardinal.aleph 1).ord

1 < ω₁.

The deterministic extension driver

theorem FirstOrder.Language.WOMem.extend_det {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) {σ χ : (L.withConstants ℕ).Sentenceω} (hσ : σ ∈ S) (hσnotatom : ∀ (q r : ℚ), σ ≠ ratLtAtom lt q r) (hχnb : χ ∉ baseDiagram φ lt) (hχU : χ ∈ GenU (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ)) (hsub : sentenceJConsts χ ⊆ sentenceJConsts σ) (hforce : ∀ (M : Type) (inst : L.Structure M), Nonempty M → ∀ (h : ℕ → M), σ.Realize M → χ.Realize M) : WOMem φ lt (S ∪ {χ})

Deterministic extension: a target whose support lies inside a non-atomic source member's support, and which is semantically forced by the source at every controlled expansion, extends the member.

C0

theorem FirstOrder.Language.WOMem.no_falsum {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) : BoundedFormulaω.falsum ∉ S

(C0a) No member contains falsum.

theorem FirstOrder.Language.WOMem.no_contradiction {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (χ : (L.withConstants ℕ).Sentenceω) : ¬(χ ∈ S ∧ BoundedFormulaω.not χ ∈ S)

(C0b) No member contains a sentence and its negation — the symmetric four-case base/remainder argument through the C0 helper.

Deterministic connective fields

theorem FirstOrder.Language.WOMem.C2_not_not {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (ψ : (L.withConstants ℕ).Sentenceω) (hσ : (BoundedFormulaω.not ψ).not ∈ S) : WOMem φ lt (S ∪ {ψ})

(C2) Double negation.

theorem FirstOrder.Language.WOMem.C1_neg_imp {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (ψ₁ ψ₂ : (L.withConstants ℕ).Sentenceω) (hσ : (BoundedFormulaω.imp ψ₁ ψ₂).not ∈ S) : WOMem φ lt (S ∪ {ψ₁}) ∧ WOMem φ lt (S ∪ {BoundedFormulaω.not ψ₂})

(C1') Negated implication: both halves.

theorem FirstOrder.Language.WOMem.C3_iInf {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hσ : BoundedFormulaω.iInf φs ∈ S) (k : ℕ) : WOMem φ lt (S ∪ {φs k})

(C3) Countable conjunction: every component.

theorem FirstOrder.Language.WOMem.C4_neg_iSup {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hσ : (BoundedFormulaω.iSup φs).not ∈ S) (k : ℕ) : WOMem φ lt (S ∪ {BoundedFormulaω.not (φs k)})

(C4') Negated disjunction: every negated component.

The branching driver

theorem FirstOrder.Language.star_all_of_unbounded {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} (h : ∀ β < (Cardinal.aleph 1).ord, ∃ (α : Ordinal.{0}), β ≤ α ∧ α < (Cardinal.aleph 1).ord ∧ StarCondition φ lt Γ α) (α : Ordinal.{0}) : α < (Cardinal.aleph 1).ord → StarCondition φ lt Γ α

Upgrading (*) from an unbounded set of levels to every level (downward closure).

theorem FirstOrder.Language.WOMem.branch_choice {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} : WOMem φ lt S → ∀ {ι : Type} [Countable ι] [Nonempty ι] (tgt : ι → (L.withConstants ℕ).Sentenceω) (hchoice : ∀ α < (Cardinal.aleph 1).ord, ∃ (i : ι), StarCondition φ lt (S \ baseDiagram φ lt ∪ {tgt i}) α), ∃ (i : ι), ∀ α < (Cardinal.aleph 1).ord, StarCondition φ lt (S \ baseDiagram φ lt ∪ {tgt i}) α

The branching driver: if every level admits some branch, one branch works at every level — the cofinal-fiber pigeonhole plus downward closure.

theorem FirstOrder.Language.WOMem.C1_imp {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (ψ₁ ψ₂ : (L.withConstants ℕ).Sentenceω) (hσ : BoundedFormulaω.imp ψ₁ ψ₂ ∈ S) : WOMem φ lt (S ∪ {BoundedFormulaω.not ψ₁}) ∨ WOMem φ lt (S ∪ {ψ₂})

(C1) Implication: one of the two branches extends.

theorem FirstOrder.Language.WOMem.C4_iSup {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hσ : BoundedFormulaω.iSup φs ∈ S) : ∃ (k : ℕ), WOMem φ lt (S ∪ {φs k})

(C4) Countable disjunction: some component extends.

theorem FirstOrder.Language.WOMem.C3_neg_iInf {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (φs : ℕ → (L.withConstants ℕ).Sentenceω) (hσ : (BoundedFormulaω.iInf φs).not ∈ S) : ∃ (k : ℕ), WOMem φ lt (S ∪ {BoundedFormulaω.not (φs k)})

(C3') Negated conjunction: some negated component extends.

Equality congruence

theorem FirstOrder.Language.WOMem.constEq_mem_rem {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} : WOMem φ lt S → ∀ {a b : ℕ} (h : constEq a b ∈ S), constEq a b ∈ S \ baseDiagram φ lt

A constant equality in a member lies in the remainder (its support is nonempty, and it is not relation-shaped).

theorem FirstOrder.Language.WOMem.extend_constEq {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) {a b : ℕ} (hab : constEq a b ∉ baseDiagram φ lt) (hsupp : sentenceJConsts (constEq a b) ⊆ ⋃ χ ∈ S \ baseDiagram φ lt, sentenceJConsts χ) (hval : ∀ α < (Cardinal.aleph 1).ord, ∀ (W : StarWitness φ lt (S \ baseDiagram φ lt) α), W.h a = W.h b) : WOMem φ lt (S ∪ {constEq a b})

Equality congruence targets: realized and covered from remainder equalities.

theorem FirstOrder.Language.WOMem.eq_symm {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (a b : ℕ) (hσ : constEq a b ∈ S) : WOMem φ lt (S ∪ {constEq b a})

Equality symmetry.

theorem FirstOrder.Language.WOMem.eq_trans {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (a b d : ℕ) (h₁ : constEq a b ∈ S) (h₂ : constEq b d ∈ S) : WOMem φ lt (S ∪ {constEq a d})

Equality transitivity.

Constant-sensitive fields

def FirstOrder.Language.StarWitness.update_nonrat {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} {α : Ordinal.{0}} (W : StarWitness φ lt Γ α) {c : ℕ} (hcr : c ∉ Set.range ratConstIdx) (hcΓ : ∀ χ ∈ Γ, c ∉ sentenceJConsts χ) (v : W.M) : StarWitness φ lt Γ α

Updating the constant map at a non-rational-range index outside the remainder's support preserves the star witness (the marking is untouched).

Equations

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

theorem FirstOrder.Language.exists_fresh_henkin {F : Set ℕ} (hF : F.Finite) : ∃ (n : ℕ), henkinConstIdx n ∉ F

A fresh Henkin index avoiding any finite set exists.

theorem FirstOrder.Language.snoc_elim0_eq_const {M : Type} (v : M) : Fin.snoc Fin.elim0 v = fun (x : Fin (0 + 1)) => v

The one-variable constant environment is the snoc environment.

theorem FirstOrder.Language.WOMem.eq_refl {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (c : ℕ) : WOMem φ lt (S ∪ {constEq c c})

Equality reflexivity (constant-sensitive: the range split).

theorem FirstOrder.Language.WOMem.all_inst {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hσ : ψ.all ∈ S) (c : ℕ) : WOMem φ lt (S ∪ {instConst c ψ})

Universal instantiation (constant-sensitive: the range split).

theorem FirstOrder.Language.WOMem.neg_all_witness {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (ψ : (L.withConstants ℕ).BoundedFormulaω Empty 1) (hσ : ψ.all.not ∈ S) : ∃ (c : ℕ), WOMem φ lt (S ∪ {BoundedFormulaω.not (instConst c ψ)})

The fresh existential witness: syntactic freshness is chosen against the finite remainder-and-source support; parity (oddness) separately places the constant outside the rational range.

theorem FirstOrder.Language.relInst_mem_baseDiagram_of_nonempty {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {l : ℕ} {R : L.Relations l} {g : Fin l → ℕ} (i : Fin l) (hb : relInst R g ∈ baseDiagram φ lt) : ∃ (q : ℚ) (r : ℚ), q < r ∧ relInst R g = ratLtAtom lt q r

A relation instance with an inhabited coordinate that lies in the base diagram is a positive diagram atom: the lifted-root alternative is eliminated by constant support (the instance mentions g i, the root mentions nothing).

theorem FirstOrder.Language.WOMem.rel_congr {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {S : Set (L.withConstants ℕ).Sentenceω} (hS : WOMem φ lt S) (l : ℕ) (R : L.Relations l) (g : Fin l → ℕ) (i : Fin l) (b : ℕ) (hσ : relInst R g ∈ S) (heq : constEq (g i) b ∈ S) : WOMem φ lt (S ∪ {relInst R (Function.update g i b)})

Relation congruence (the fifteenth field): one-coordinate replacement along a remainder equality. Remainder/root sources use ordinary equality congruence in the approximating model; a diagram-atom source first marks both endpoints at a positive level, obtains the atom through the chain, and descends.