Marking extension: the range-based constant split (issue #12, commit 4b part 2)

The constant-sensitive closure rules split an arbitrary constant c by c ∈ Set.range ratConstIdx — not by parity coding (per review: ratConstIdx is injective but not proved surjective onto the evens; unused even indices are treated exactly like Henkin constants, as ordinary auxiliary constants with no rank insertion).

• henkinConstIdx_notMem_range_ratConstIdx — fresh existential witnesses chosen odd are automatically outside the rational range.
• add_lt_omega1 / add_one_lt_omega1 — ω₁ is closed under the (*)-level arithmetic the fields need (β := α + α + 1).
• exists_insertNth_slot — an unmarked rational has a slot at which inserting it keeps the marking enumeration strictly monotone (via the initial-segment characterization of the below-q₀ marks).
• StarWitness.add_sentence — the generic closure step: a sentence realized by the witness whose rationals are already marked extends the remainder.
• StarWitness.mark_rat — the composite rational-marking operation: an unmarked rational is re-pointed to an engine-provided chain point (GapWitness.exists_insertNth) at the strict- monotonicity slot; freshness for the remainder is automatic (an unmarked rational cannot be mentioned, by mark_cover), so remainder realization transports by the repointing invariant. Already-marked rationals need only downward closure.

The range split

theorem FirstOrder.Language.henkinConstIdx_notMem_range_ratConstIdx (n : ℕ) : henkinConstIdx n ∉ Set.range ratConstIdx

Odd (Henkin) constants lie outside the rational range — parity.

ω₁ arithmetic

theorem FirstOrder.Language.add_lt_omega1 {α β : Ordinal.{0}} (hα : α < (Cardinal.aleph 1).ord) (hβ : β < (Cardinal.aleph 1).ord) : α + β < (Cardinal.aleph 1).ord

ω₁ is closed under addition.

theorem FirstOrder.Language.add_one_lt_omega1 {α : Ordinal.{0}} (hα : α < (Cardinal.aleph 1).ord) : α + 1 < (Cardinal.aleph 1).ord

ω₁ is closed under successor.

The strict-monotonicity slot

theorem FirstOrder.Language.range_insertNth {m : ℕ} {γ : Type u_1} (s : Fin (m + 1)) (x : γ) (f : Fin m → γ) : Set.range (s.insertNth x f) = insert x (Set.range f)

The range of an inserted tuple.

theorem FirstOrder.Language.exists_insertNth_slot {m : ℕ} {mark : Fin m → ℚ} (hm : StrictMono mark) {q₀ : ℚ} (hq : q₀ ∉ Set.range mark) : ∃ (s : Fin (m + 1)), StrictMono (s.insertNth q₀ mark)

The slot lemma: an unmarked rational has a slot at which insertion keeps the enumeration strictly monotone.

The generic closure step

def FirstOrder.Language.StarWitness.add_sentence {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} {α : Ordinal.{0}} (W : StarWitness φ lt Γ α) {χ : (L.withConstants ℕ).Sentenceω} (hreal : χ.Realize W.M) (hsupp : ∀ (q : ℚ), ratConstIdx q ∈ sentenceJConsts χ → q ∈ Set.range W.mark) : StarWitness φ lt (Γ ∪ {χ}) α

Adding a realized, already-covered sentence: a sentence realized by the witness whose mentioned rationals are all marked extends the remainder without touching the marking.

Equations

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

The composite rational-marking operation

theorem FirstOrder.Language.StarWitness.mark_rat {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} {α β : Ordinal.{0}} (W : StarWitness φ lt Γ β) (hβ : α + α < β) (q₀ : ℚ) : ∃ (W' : StarWitness φ lt Γ α), q₀ ∈ Set.range W'.mark ∧ Set.range W.mark ⊆ Set.range W'.mark

Marking a rational (the range-split case 1): from a witness at β with α + α < β, produce a witness at α whose marking covers q₀. Already-marked rationals need only downward closure; an unmarked rational is automatically fresh for the remainder (mark_cover), so its constant re-points to the engine's chain point at the strict-monotonicity slot.