Lyndon interpolation, countable relational core (issue #14, Unit 5, commit 2)

The internal countable joint-language theorem: over a countable relational vocabulary, an entailment r₁ ⊨ r₂ admits an interpolant whose positive relation occurrences lie in both roots' positive occurrences and whose negative occurrences lie in both roots' negative ones.

This is the relation-polarity / logical-equality form of López–Escobar 1965, Theorem 4.1: clause (.4) in full, with (.3)'s equality-occurrence condition deliberately not claimed (equality is logical here and unconstrained in the interpolant).

The skeleton is Craig's, unchanged: assume no interpolant, observe that the mapped root pair is then inseparable at empty support (an empty-support separator would strip, through the signed root gate, to a base interpolant with all three bounds), and feed the inseparable pair to the polarity-refined paired model existence. The resulting single model realizes r₁ and refutes r₂, contradicting the entailment.

The root orientation is cited, not re-derived. The Δ-root is r₂.not carrying its own polarity bounds (Pos (r₂.not), Neg (r₂.not)), so the engine maintains the class (Pos r₁ ∩ Neg (r₂.not), Neg r₁ ∩ Pos (r₂.not)); lyndon_root_class_eq is what turns that into the endpoint's (Pos r₁ ∩ Pos r₂, Neg r₁ ∩ Neg r₂).

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

Lyndon interpolation, countable relational core.