The sole Löwenheim–Skolem consumer (issue #10, Unit 4 commit 3)

FragmentLowenheimSkolem is imported only here. From a glued model of both side sentences, a countable fragment-elementary substructure models both; the tagged zero-ary witness c's graph-totality axiom bootstraps its nonemptiness; reconstruction plus numMap_bijective make it infinite; transported to ℕ it yields a single code lying in both B (pcClass_eq with hinv) and Bᶜ (pcClass_eq with hinv.compl) — a contradiction.

Endpoints: pcMem_disjoint and pcSentences_entails_not, the latter being exactly what Unit 5 feeds to craig_pcSeparation_relational.

instance FirstOrder.Language.instCountableSigmaNatFunctionsGraphLanguageKLang {L : Language} : Countable ((n : ℕ) × L.KLang.graphLanguage.Functions n)

theorem FirstOrder.Language.pcMem_disjoint {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {B : Set L.StructureSpace} (T₀ T₁ : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (hT₀ : ∀ (c : L.StructureSpace), c ∈ B ↔ ∃ (g : ℕ → ℕ), ∀ (n : ℕ), (fun (i : Fin n) => queryCode c ↑i, fun (i : Fin n) => g ↑i) ∈ T₀ n) (hT₁ : ∀ (c : L.StructureSpace), c ∈ Bᶜ ↔ ∃ (g : ℕ → ℕ), ∀ (n : ℕ), (fun (i : Fin n) => queryCode c ↑i, fun (i : Fin n) => g ↑i) ∈ T₁ n) (hinv : IsomorphismInvariant B) (M : Type) [instL : L.Structure M] : ¬(PCMem baseGraphEmb (L.pcSentence PCSide.left T₀) M ∧ PCMem baseGraphEmb (L.pcSentence PCSide.right T₁) M)

Projective-class disjointness (the sole IsomorphismInvariant × downward-LS consumer): if B's tree is T₀ and Bᶜ's is T₁, no base model is simultaneously in the projective classes of the two side sentences.

theorem FirstOrder.Language.pcSentences_entails_not {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {B : Set L.StructureSpace} (T₀ T₁ : (n : ℕ) → Set ((Fin n → Bool) × (Fin n → ℕ))) (hT₀ : ∀ (c : L.StructureSpace), c ∈ B ↔ ∃ (g : ℕ → ℕ), ∀ (n : ℕ), (fun (i : Fin n) => queryCode c ↑i, fun (i : Fin n) => g ↑i) ∈ T₀ n) (hT₁ : ∀ (c : L.StructureSpace), c ∈ Bᶜ ↔ ∃ (g : ℕ → ℕ), ∀ (n : ℕ), (fun (i : Fin n) => queryCode c ↑i, fun (i : Fin n) => g ↑i) ∈ T₁ n) (hinv : IsomorphismInvariant B) : (L.pcSentence PCSide.left T₀).Entails (BoundedFormulaω.not (L.pcSentence PCSide.right T₁))

The entailment endpoint — exactly what Unit 5 feeds to Craig PC-separation: no model satisfies both side sentences, so the left entails the negation of the right.