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.

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.