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

The deterministic extension driver

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

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