Reconstruction and the code-class equality (issue #10, Unit 3b)

The converse of Unit 3a: reconstruct the functional KLang-structure from a model of the PC sentence, read a branch off it, and land the base reduct back in B — the only place IsomorphismInvariant is consumed. The endpoints:

• pcClass_subset (needs invariance) — codeReduct '' ModelsOf (pcSentence side T) ⊆ B;
• subset_pcClass (Unit 3a, no invariance) — B ⊆ codeReduct '' ModelsOf (pcSentence side T);
• pcClass_eq (needs invariance) — the code-class equality codeReduct '' ModelsOf (pcSentence side T) = B.

instance FirstOrder.Language.instCountableFunctionsOfRelational {L : Language} [L.IsRelational] : Countable ((n : ℕ) × L.Functions n)

theorem FirstOrder.Language.pcClass_subset_of_invariant_superset {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {B W : Set L.StructureSpace} (side : PCSide) (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) (hBW : B ⊆ W) (hWinv : IsomorphismInvariant W) : codeReduct '' ModelsOf (L.pcSentence side T) ⊆ W

Converse gate, through an invariant envelope: the base reducts of the PC class lie in any isomorphism-invariant W ⊇ B. This is the sole consumer of IsomorphismInvariant.

B itself need not be invariant, which is what makes this usable for an arbitrary analytic family: a sentence-defined reduct class is always invariant, so codeReduct '' ModelsOf Θ = B is unachievable for non-invariant B, but the sandwich

B ⊆ codeReduct '' ModelsOf Θ ⊆ W

is available for every invariant W ⊇ B and is what boundedness arguments actually consume. pcClass_subset is the specialization W := B.

theorem FirstOrder.Language.pcClass_subset {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {B : Set L.StructureSpace} (side : PCSide) (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) (hinv : IsomorphismInvariant B) : codeReduct '' ModelsOf (L.pcSentence side T) ⊆ B

Converse gate (pcClass_subset): the base reducts of the PC class lie in B, when B itself is invariant. The W := B specialization of pcClass_subset_of_invariant_superset.

theorem FirstOrder.Language.pcClass_eq {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {B : Set L.StructureSpace} (side : PCSide) (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) (hinv : IsomorphismInvariant B) : codeReduct '' ModelsOf (L.pcSentence side T) = B

The code-class equality (needs invariance): the base reducts of the PC class are exactly B.