The type-preserving back-and-forth (issue #17 chunk 3)

The relation TypeAgree N a b: tuples of the ambient M and of the companion substructure N agree when their complete L_{ω₁ω}-types — both computed IN M, viewing b through the inclusion — coincide. The two extension properties hold by the isolator machinery:

• forth (TypeAgree.forth): isolate tp_M(ā, a'); its one-variable existential holds at ā, transfers to ι b̄ across the type equality, descends to N by A-elementarity of the controlling fragment, and the witness comes back up at arity n+1;
• back (TypeAgree.back): isolate tp_M(ι b̄, ι b'); its existential transfers across the type equality to ā, and the witness is chosen directly in M — no A-elementarity.

The audited thin bridge (bfEquiv_all_of_typeAgree): any relation with type agreement and the two extensions is BFEquiv at EVERY ordinal — one limitRecOn induction whose zero stage is TypeAgree.sameAtomicType (atomic indices are realizations of atomic L_{ω₁ω}-formulas, and the substructure inclusion reflects them).

def FirstOrder.Language.TypeAgree {L : Language} {M : Type} [L.Structure M] (N : L.Substructure M) {n : ℕ} (a : Fin n → M) (b : Fin n → ↥N) : Prop

Type agreement: the complete types in the AMBIENT structure coincide.

Equations

• FirstOrder.Language.TypeAgree N a b = (FirstOrder.Language.infinitaryType M a = FirstOrder.Language.infinitaryType M fun (i : Fin n) => ↑(b i))

theorem FirstOrder.Language.typeAgree_elim0 {L : Language} {M : Type} [L.Structure M] (N : L.Substructure M) : TypeAgree N Fin.elim0 Fin.elim0

theorem FirstOrder.Language.TypeAgree.realize_iff {L : Language} {M : Type} [L.Structure M] {N : L.Substructure M} {n : ℕ} {a : Fin n → M} {b : Fin n → ↥N} (h : TypeAgree N a b) (φ : L.BoundedFormulaω Empty n) : φ.Realize Empty.elim a ↔ φ.Realize Empty.elim fun (i : Fin n) => ↑(b i)

theorem FirstOrder.Language.TypeAgree.forth {L : Language} {M : Type} [L.Structure M] {hsmall : Lomega1omegaSmall M} {N : L.Substructure M} (hAe : AElementary (isolatorFragment hsmall) N.subtype) {n : ℕ} {a : Fin n → M} {b : Fin n → ↥N} (hab : TypeAgree N a b) (a' : M) : ∃ (b' : ↥N), TypeAgree N (Fin.snoc a a') (Fin.snoc b b')

Forth: every ambient element has a companion match extending the agreement.

theorem FirstOrder.Language.TypeAgree.back {L : Language} {M : Type} [L.Structure M] (hsmall : Lomega1omegaSmall M) {N : L.Substructure M} {n : ℕ} {a : Fin n → M} {b : Fin n → ↥N} (hab : TypeAgree N a b) (b' : ↥N) : ∃ (a' : M), TypeAgree N (Fin.snoc a a') (Fin.snoc b b')

Back: every companion element has an ambient match — the witness is chosen directly in M; no A-elementarity is consumed.

theorem FirstOrder.Language.TypeAgree.sameAtomicType {L : Language} {M : Type} [L.Structure M] {N : L.Substructure M} {n : ℕ} {a : Fin n → M} {b : Fin n → ↥N} (hab : TypeAgree N a b) : SameAtomicType a b

The zero stage: type agreement gives atomic agreement — atomic indices are realizations of atomic L_{ω₁ω}-formulas, and the inclusion reflects them.

theorem FirstOrder.Language.bfEquiv_all_of_typeAgree {L : Language} {M : Type} [L.Structure M] {N : L.Substructure M} (hforth : ∀ {n : ℕ} (a : Fin n → M) (b : Fin n → ↥N), TypeAgree N a b → ∀ (a' : M), ∃ (b' : ↥N), TypeAgree N (Fin.snoc a a') (Fin.snoc b b')) (hback : ∀ {n : ℕ} (a : Fin n → M) (b : Fin n → ↥N), TypeAgree N a b → ∀ (b' : ↥N), ∃ (a' : M), TypeAgree N (Fin.snoc a a') (Fin.snoc b b')) (α : Ordinal.{u_1}) {n : ℕ} (a : Fin n → M) (b : Fin n → ↥N) : TypeAgree N a b → BFEquiv α n a b

The audited thin bridge: a type-agreeing relation with the forth and back extensions is back-and-forth equivalent at EVERY ordinal.

The semantic countable-companion theorem (chunk 4)

theorem FirstOrder.Language.bfEquiv_all_of_companion {L : Language} {M : Type} [L.Structure M] {hsmall : Lomega1omegaSmall M} {N : L.Substructure M} (hAe : AElementary (isolatorFragment hsmall) N.subtype) (α : Ordinal.{u_1}) : BFEquiv α 0 Fin.elim0 Fin.elim0

Back-and-forth equivalence with a given companion (identity-keeping form): any countable companion from chunk 2 is BFEquiv at every ordinal with the ambient structure.

theorem FirstOrder.Language.exists_countable_bfEquiv_of_lomega1omegaSmall {L : Language} {M : Type} [L.Structure M] [Countable ((n : ℕ) × L.Functions n)] (hsmall : Lomega1omegaSmall M) : ∃ (N : Type) (x : L.Structure N), Countable N ∧ ∀ (α : Ordinal.{u_1}), BFEquiv α 0 Fin.elim0 Fin.elim0

The semantic countable-companion theorem (issue #17 chunk 4 endpoint): a small structure over countably many function symbols has a countable model back-and-forth equivalent to it at every ordinal.

theorem FirstOrder.Language.realize_inf_iff_of_companion {L : Language} {M : Type} [L.Structure M] [L.IsRelational] {hsmall : Lomega1omegaSmall M} {N : L.Substructure M} (hAe : AElementary (isolatorFragment hsmall) N.subtype) (φ : L.BoundedFormulaInf (Fin 0) 0) : FormulaInf.Realize φ Fin.elim0 ↔ FormulaInf.Realize φ Fin.elim0

All-L_∞ω-formula agreement with a companion — the relational packaging boundary (BFEquiv_implies_agreeQR).