Smallness of the local EM model (issue #11 unit 4)

The conditional countability theorem: over a highly order-transitive skeleton and a countable base language, the local EM carrier realizes only countably many complete L_{ω₁ω}-types at every arity (LocalEMContext.lomega1omegaSmall), for the rich localColim-reduct structure structureBase.

The argument avoids any orbit quotient, via code FIBERS: for each tuple code c, CodeTypes c is the set of realized types of tuples with code c. The orbit theorem plus formula invariance under the induced automorphisms make each fiber SUBSINGLETON (codeTypes_subsingleton), the realized types are exactly the union of the fibers over the countable code type (realizedTypes_eq_iUnion_codeTypes — set extensionality), and a countable union of subsingletons is countable. Transport to the original language is Lomega1omegaSmall.of_expansion (ModelTheory/InfinitaryTypes.lean), not re-proved here.

def FirstOrder.Language.LocalEMContext.CodeTypes {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) {n : ℕ} (c : Λ.LocalEMTupleCode n) : Set (Set (Λ.BoundedFormulaω Empty n))

The fiber of realized types over a tuple code: the types of tuples whose code is c.

Equations

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

theorem FirstOrder.Language.LocalEMContext.codeTypes_subsingleton {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (hJ : HighlyOrderTransitive J) {n : ℕ} (c : Λ.LocalEMTupleCode n) : (ctx.CodeTypes c).Subsingleton

Each code fiber is subsingleton: tuples with the same code lie in one orbit of the induced automorphisms (exists_carrierEquiv_of_tupleCode_eq), and every infinitary formula is invariant under those automorphisms (realize_carrierEquiv), so they realize the same type.

theorem FirstOrder.Language.LocalEMContext.realizedTypes_eq_iUnion_codeTypes {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (n : ℕ) : RealizedInfinitaryTypes (Carrier Λ J ctx) n = ⋃ (c : Λ.LocalEMTupleCode n), ctx.CodeTypes c

The realized types are the union of the code fibers — set extensionality.

theorem FirstOrder.Language.LocalEMContext.lomega1omegaSmall {Λ : Language} {J : Type} [LinearOrder J] {M : Type} [Λ.Structure M] (ctx : Λ.LocalEMContext J) (hJ : HighlyOrderTransitive J) [Countable ((l : ℕ) × Λ.Functions l)] : Lomega1omegaSmall (Carrier Λ J ctx)

The conditional smallness theorem (issue #11 unit 4): over a highly order-transitive skeleton and a countable base language, the local EM carrier — with its rich localColim-reduct structure — realizes only countably many complete L_{ω₁ω}-types at every arity.