Craig separation (PC-separation) for L_ω₁ω, relational (issue #8, audit §10)

The disjunction form of Craig interpolation, in the shared-vocabulary symbSublang packaging frozen by the audit (§10). Two sentences ψ₁, ψ₂ with no common model (ψ₁ ⊨ ¬ψ₂) are separated by a single sentence θ₀ of their shared vocabulary L₀ = symbSublang (F₁∩F₂) (R₁∩R₂): θ₀ holds in the L₀-reduct of every model of ψ₁ and fails in the L₀-reduct of every model of ψ₂.

craig_pcSeparation_relational [L.IsRelational] :
  Sentenceω.Entails ψ₁ ψ₂.not →
    ∃ θ₀ : (symbSublang (ψ₁.functionsIn ∩ ψ₂.functionsIn)
                        (ψ₁.relationsIn ∩ ψ₂.relationsIn)).Sentenceω,
      (∀ M ⊨ ψ₁, the L₀-reduct of M realizes θ₀) ∧
      (∀ M ⊨ ψ₂, the L₀-reduct of M refutes θ₀)

This is the #8-side deliverable consumed by #10; #10 owns the general PC-class packaging and may re-express the shared vocabulary through its own Language-inclusion representation. The derivation is the audited one: interpolate ψ₁ ⊨ ¬ψ₂, whose interpolant θ has symbols in the intersection (functionsIn_not/relationsIn_not strip the negation), then restrictSymbols it into L₀ and read both directions off the reduct realization bridge (realize_mapLanguage).

theorem FirstOrder.Language.craig_pcSeparation_relational {L : Language} [L.IsRelational] (ψ₁ ψ₂ : L.Sentenceω) (h : ψ₁.Entails (BoundedFormulaω.not ψ₂)) : ∃ (θ₀ : (symbSublang (BoundedFormulaω.functionsIn ψ₁ ∩ BoundedFormulaω.functionsIn ψ₂) (BoundedFormulaω.relationsIn ψ₁ ∩ BoundedFormulaω.relationsIn ψ₂)).Sentenceω), (∀ (M : Type) [inst : L.Structure M] [Nonempty M], ψ₁.Realize M → θ₀.Realize M) ∧ ∀ (M : Type) [inst : L.Structure M] [Nonempty M], ψ₂.Realize M → ¬θ₀.Realize M

Craig separation (PC-separation), relational. If ψ₁ and ψ₂ have no common model (ψ₁ ⊨ ¬ψ₂), a single shared-vocabulary sentence θ₀ separates them: it holds in the shared-vocabulary reduct of every model of ψ₁ and fails in that of every model of ψ₂.