Realization helpers for the closure fields (issue #12, commit 4b part 1)

The shared semantic tools the fifteen closure fields consume, isolated per review:

• realize_lift_wc — the constant-free lift bridge: φ̂ holds at the controlled expansion iff φ holds in the base structure.
• sentenceJConsts_lift_eq_empty — the lift mentions no constants (its functionsIn image consists of Sum.inl symbols only).
• The C0 helper (StarWitness.realize_base_of_opposite): a base member whose opposite lies in the finite remainder is realized at level 1 — split into the lifted-root case (the bridge) and the positive-diagram case (the opponent's support + mark_cover + realize_marked_atom). C0_no_contradiction then becomes a symmetric four-case base/remainder argument with no symbol/support bookkeeping inside the packaged field.
• The repointing invariant (StarWitness.rem_realize_update): updating the constant interpretation at an index absent from the remainder's support preserves remainder realization (realize_congr_const). Reused by eq_refl, all_inst, and the fresh witness case.
• Shape/support facts about baseDiagram members (mem_baseDiagram_elim, not_mem_baseDiagram_elim, sentenceJConsts_ratLtAtom, not_ne_self, lift_eq_falsum_reflect).

The constant-free lift

theorem FirstOrder.Language.realize_lift_wc {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) (φ : L.Sentenceω) : Sentenceω.Realize (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) M ↔ φ.Realize M

The lift bridge: the lifted root holds at the controlled expansion iff the root holds in the base structure.

theorem FirstOrder.Language.sentenceJConsts_lift_eq_empty {L : Language} (φ : L.Sentenceω) : sentenceJConsts (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ) = ∅

The lift mentions no constants.

Shape and support of base-diagram members

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

A base-diagram member is the lifted root or a positive diagram atom.

theorem FirstOrder.Language.BoundedFormulaω.not_ne_self {L' : Language} {α : Type} {n : ℕ} (φ : L'.BoundedFormulaω α n) : φ.not ≠ φ

No formula equals its own negation.

theorem FirstOrder.Language.not_mem_baseDiagram_elim {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {χ : (L.withConstants ℕ).Sentenceω} (h : BoundedFormulaω.not χ ∈ baseDiagram φ lt) : BoundedFormulaω.not χ = BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ

A negation in the base diagram is the lifted root (atoms are relation-shaped).

theorem FirstOrder.Language.sentenceJConsts_ratLtAtom {L : Language} (lt : L.Relations 2) (q r : ℚ) : sentenceJConsts (ratLtAtom lt q r) = {ratConstIdx q, ratConstIdx r}

The constant support of a positive diagram atom.

theorem FirstOrder.Language.lift_eq_falsum_reflect {L : Language} {φ : L.Sentenceω} (h : BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ = BoundedFormulaω.falsum) : φ = BoundedFormulaω.falsum

The lift reflects falsum.

The C0 helper

theorem FirstOrder.Language.StarWitness.realize_base_of_opposite {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} (W : StarWitness φ lt Γ 1) {χ : (L.withConstants ℕ).Sentenceω} (hχ : χ ∈ baseDiagram φ lt) (hopp : BoundedFormulaω.not χ ∈ Γ) : χ.Realize W.M

A base member whose opposite lies in the finite remainder is realized at level 1: the lifted root through the bridge, a positive diagram atom through the opponent's support, mark_cover, and the derived diagram.

The repointing invariant

theorem FirstOrder.Language.StarWitness.rem_realize_update {L : Language} {φ : L.Sentenceω} {lt : L.Relations 2} {Γ : Set (L.withConstants ℕ).Sentenceω} {α : Ordinal.{0}} (W : StarWitness φ lt Γ α) {c : ℕ} (hc : ∀ χ ∈ Γ, c ∉ sentenceJConsts χ) (x : W.M) (χ : (L.withConstants ℕ).Sentenceω) : χ ∈ Γ → χ.Realize W.M

Repointing a constant absent from the remainder's support preserves remainder realization — the invariant behind every constant rule (eq_refl, all_inst, the fresh witness).