Constant abstraction and reinterpretation surgery (issue #8 kernel steps 3–5) #

The genuinely uncertain freshness mechanism of the Craig interpolation arc (docs/craig-audit.md §6a). Over a constant expansion L[[ℕ]] with a fixed base L-structure on M:

BoundedFormulaω.realize_congr_instances — realization depends only on the interpretation of the symbols (two L-structure instances agreeing on all funMap/RelMap values realize identically). Used for the ambient bridge.
wc base h — the L[[ℕ]]-structure with base reduct base and constants interpreted by h : ℕ → M; ambient_realize_iff_wc bridges an arbitrary ambient L[[ℕ]]-structure to this controlled form.
realize_congr_const — realization is unchanged by altering the constant interpretation off the formula's constant support (sentenceJConsts); the invariance-outside-support engine (Claim A of the acceptance argument).
BoundedFormulaω.abstractConst j — withdraw the constant c_j into the free variable 0 (Empty-based → Fin 1-based), with the occurrence-deletion lemma.
realize_abstractConst — the reinterpretation engine (Claim B): realizing the abstracted formula at a witness a equals realizing the original with c_j reinterpreted to a.

Pure realization surgery: no InsepAt, no interpolation-specific commitments.

Two-instance realization congruence #

source

theorem FirstOrder.Language.Term.realize_congr_instances {L : Language} {M α : Type} (S S' : L.Structure M) (hf : ∀ {l : ℕ} (f : L.Functions l) (x : Fin l → M), Structure.funMap f x = Structure.funMap f x) (v : α → M) (t : L.Term α) :

realize v t = realize v t

Term realization depends only on the funMap values: two L-structure instances agreeing on every funMap realize every term identically.

source

theorem FirstOrder.Language.BoundedFormulaω.realize_congr_instances {L : Language} {M α : Type} (S S' : L.Structure M) (hf : ∀ {l : ℕ} (f : L.Functions l) (x : Fin l → M), Structure.funMap f x = Structure.funMap f x) (hr : ∀ {l : ℕ} (R : L.Relations l) (x : Fin l → M), Structure.RelMap R x ↔ Structure.RelMap R x) {n : ℕ} (φ : L.BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) :

φ.Realize v xs ↔ φ.Realize v xs

Realization depends only on the funMap/RelMap values: two L-structure instances agreeing on all interpretations realize every formula identically.

The controlled single-layer structure `wc base h` #

source

@[reducible]

def FirstOrder.Language.wc {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) :

(L.withConstants ℕ).Structure M

The L[[ℕ]]-structure on M with base reduct base and constants interpreted by h.

Equations

FirstOrder.Language.wc base h = L.withConstantsStructure ℕ

Instances For

source

@[simp]

theorem FirstOrder.Language.wc_funMap_inl {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) {l : ℕ} (f : L.Functions l) (x : Fin l → M) :

Structure.funMap (Sum.inl f) x = Structure.funMap f x

source

@[simp]

theorem FirstOrder.Language.wc_funMap_inr {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) (k : ℕ) (x : Fin 0 → M) :

Structure.funMap (Sum.inr k) x = h k

source

@[simp]

theorem FirstOrder.Language.wc_relMap_inl {L : Language} {M : Type} (base : L.Structure M) (h : ℕ → M) {l : ℕ} (R : L.Relations l) (x : Fin l → M) :

Structure.RelMap (Sum.inl R) x = Structure.RelMap R x

source

def FirstOrder.Language.ambientConstMap {L : Language} (M : Type) [S : (L.withConstants ℕ).Structure M] (k : ℕ) :

The interpretation of the constant c_k by an ambient L[[ℕ]]-structure.

Equations

FirstOrder.Language.ambientConstMap M k = FirstOrder.Language.Structure.funMap (Sum.inr k) Fin.elim0

Instances For

source

theorem FirstOrder.Language.ambient_realize_iff_wc {L : Language} {M α : Type} [S : (L.withConstants ℕ).Structure M] {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω α n) (v : α → M) (xs : Fin n → M) :

φ.Realize v xs ↔ φ.Realize v xs

The ambient bridge: any ambient L[[ℕ]]-structure realizes exactly as the controlled structure built from its base reduct and its constant interpretation.

Invariance outside the constant support #

source

theorem FirstOrder.Language.Term.realize_congr_const {L : Language} {M α : Type} (base : L.Structure M) {h h' : ℕ → M} {n : ℕ} (t : (L.withConstants ℕ).Term (α ⊕ Fin n)) (hagree : ∀ (k : (constantsOn ℕ).Functions 0), ⟨0, Sum.inr k⟩ ∈ t.functionsIn → h k = h' k) (w : α ⊕ Fin n → M) :

realize w t = realize w t

Two constant maps agreeing on a term's constant support give the term the same value.

source

theorem FirstOrder.Language.BoundedFormulaω.realize_congr_const {L : Language} {M α : Type} (base : L.Structure M) {h h' : ℕ → M} {n : ℕ} (φ : (L.withConstants ℕ).BoundedFormulaω α n) :

(∀ k ∈ sentenceJConsts φ, h k = h' k) → ∀ (v : α → M) (xs : Fin n → M), φ.Realize v xs ↔ φ.Realize v xs

Invariance outside the constant support (Claim A): altering the constant interpretation off a formula's constant support does not change its realization.