The Malitz root gate (issue #15)

Neutral companion to LyndonRootGate.lean. Where the Lyndon gate carries signed relation occurrences through the strip, this one carries the quantifier class: an empty-support universal L[[ℕ]]-separator strips to a genuine universal base-language interpolant.

Nothing here is new semantics. The entailment transport is the existing reduct bridge (entails_reduct_of_entails_map), the occurrence bounds are the existing stripConsts lemmas, and universality is the class-preservation lemma proved alongside stripConsts itself. This file is composition only.

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

The Malitz root gate: an empty-support universal L[[ℕ]]-separator of the mapLanguage-images of (Γ₀, Δ₀) strips to a base-language interpolant that is still universal and whose function and relation occurrences are bounded by the separator's base sets.

Constant-freeness has done its work by this point and disappears from the conclusion, which is what lets the public theorem avoid exposing any Henkin bookkeeping.