Realized-type isolators (issue #17 chunk 1)

The decisive lemma of the small-model → complete-sentence chain, stated LANGUAGE-GENERAL (independent of fragments, Löwenheim–Skolem, Scott infrastructure, and relationality, per the frozen audit): in a structure realizing only countably many complete n-types, every realized type p is ISOLATED AMONG THE REALIZED TYPES by a single L_{ω₁ω}-formula

χ_p = ⋀_{q realized} θ_{p,q},

where θ_{p,q} is an oriented separator (true at realizers of p, false at realizers of q; a membership-difference formula or its negation) and the countable conjunction is ciInf over the countable subtype of realized types. Both the language and the structure live in arbitrary universes: the subtype of realized types lands in Type (max u v), and ciInf encodes an index of any universe into the fixed ℕ carrier. "Language-general" means arbitrary function and relation symbols, no relationality assumption. The characterization:

realize_isolatingFormula_iff : χ_p.Realize Empty.elim a ↔ infinitaryType M a = p.

noncomputable def FirstOrder.Language.isolatingFormula {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (hcount : (RealizedInfinitaryTypes M n).Countable) (p : Set (L.BoundedFormulaω Empty n)) : L.BoundedFormulaω Empty n

The isolating formula χ_p of a realized type, over a structure with countably many realized n-types: the countable conjunction of the oriented separators against every realized type (a tautology at p itself).

Equations

• One or more equations did not get rendered due to their size.

theorem FirstOrder.Language.realize_isolatingFormula_iff {L : Language} {M : Type w} [L.Structure M] {n : ℕ} (hcount : (RealizedInfinitaryTypes M n).Countable) (p : Set (L.BoundedFormulaω Empty n)) (a : Fin n → M) : (isolatingFormula hcount p).Realize Empty.elim a ↔ infinitaryType M a = p

The decisive characterization: χ_p holds at a tuple exactly when its complete type is p.

Universe regression

These instantiate the characterization at a nonzero universe and at universe zero. They are compiled, so they fail if the development is ever reconstrained; the variable block alone would not catch that, since a Language.{u, v} binder can still be silently pinned by a downstream lemma.