The semantic root gate (issue #8 tranche 1.5 item 2)

At the root of the interpolation argument the allowed constant support is empty, so any separator is constant-free and strips to a base-language sentence (stripConsts). This file turns that syntactic left inverse into the semantic bridge the argument needs:

• entails_reduct_of_entails_map — a cross-language entailment bridge: an L[[ℕ]]-entailment between mapLanguage-images descends to the base L-entailment (lift every base structure by dummy constants; realization of a mapLanguage-image is realization in the reduct);
• base_interpolant_of_empty_support_separator — an empty-support L[[ℕ]]-separator strips to an actual base-language interpolant with the correct symbol-occurrence bounds and both L-entailments. This makes "InsepAt ∅ yields no base interpolant" a theorem, not a documented future composition.

theorem FirstOrder.Language.entails_reduct_of_entails_map {L : Language} {Γ₀ : Set L.Sentenceω} {φ : L.Sentenceω} (hE : Theoryω.Entails (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' Γ₀) (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) φ)) : Theoryω.Entails Γ₀ φ

Cross-language entailment bridge: if the mapLanguage-images of Γ₀ entail the mapLanguage-image of φ over L[[ℕ]], then Γ₀ entails φ over L. Proof: lift an arbitrary base model by interpreting every fresh constant as a fixed element; realization of a mapLanguage-image equals realization in the reduct (realize_mapLanguage).

theorem FirstOrder.Language.base_interpolant_of_empty_support_separator {L : Language} {Γ₀ Δ₀ : Set L.Sentenceω} (σ : (L.withConstants ℕ).Sentenceω) (hsupp : sentenceJConsts σ ⊆ ∅) (hΓ : Theoryω.Entails (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' Γ₀) σ) (hΔ : Theoryω.Entails (BoundedFormulaω.mapLanguage (L.lhomWithConstants ℕ) '' Δ₀) (BoundedFormulaω.not σ)) : ∃ (θ₀ : L.Sentenceω), BoundedFormulaω.functionsIn θ₀ ⊆ BoundedFormulaω.baseFunctionsIn σ ∧ BoundedFormulaω.relationsIn θ₀ ⊆ BoundedFormulaω.baseRelationsIn σ ∧ Theoryω.Entails Γ₀ θ₀ ∧ Theoryω.Entails Δ₀ (BoundedFormulaω.not θ₀)

The root gate: an empty-support L[[ℕ]]-separator of the mapLanguage-images of (Γ₀, Δ₀) strips to a genuine base-language interpolant — a sentence with symbols bounded by the separator's base symbols, entailed by Γ₀ and refuting Δ₀.