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, a'); its one-variable existential holds at a, 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 a, 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 w} [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.realize_iff {L : Language} {M : Type w} [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 w} [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 w} [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.

The semantic countable-companion theorem (chunk 4)

theorem FirstOrder.Language.bfEquiv_all_of_companion {L : Language} {M : Type w} [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.