Malitz interpolation, countable relational core (issue #15)

The internal countable joint-language theorem: over a countable relational vocabulary, an entailment r₁ ⊨ r₂ with universal consequent admits a universal interpolant whose occurrences lie in both roots'.

The skeleton is Craig's and Lyndon's, unchanged. Assume no interpolant; observe that the mapped root pair is then budget-inseparable — a budgeted separator would collapse (universal because the right root carries no universal occurrence, constant-free because the left root's support is empty) and strip, through the Malitz root gate, to a base interpolant with both bounds. Feed the inseparable pair to the model endpoint; the resulting model realizes r₁ and refutes r₂, contradicting the entailment.

Why universality is available at the separator. The engine's right root is r₂.not, and r₂ being universal means exactly that r₂.not has no positive universal occurrence. The right quantifier permission is therefore unusable, which is what isUniversal_of_budgetedPairSeparates converts into universality of the separator. This is the sense in which the labelled budget "pays for" the interpolant's class.

theorem FirstOrder.Language.malitz_interpolation_relational_countable {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (r₁ r₂ : L.Sentenceω) (h₂ : BoundedFormulaω.IsUniversal r₂) (h : r₁.Entails r₂) : ∃ (θ : L.Sentenceω), BoundedFormulaω.IsUniversal θ ∧ BoundedFormulaω.functionsIn θ ⊆ BoundedFormulaω.functionsIn r₁ ∩ BoundedFormulaω.functionsIn r₂ ∧ BoundedFormulaω.relationsIn θ ⊆ BoundedFormulaω.relationsIn r₁ ∩ BoundedFormulaω.relationsIn r₂ ∧ r₁.Entails θ ∧ θ.Entails r₂

Malitz interpolation, countable relational core.