Small models of every infinite size: the countable-symbol core (issue #11 unit 7a)

Marker, Theorem 11.2, countable-symbol core: if φ has arbitrarily large models then for every infinite κ it has a model of size EXACTLY κ realizing only countably many complete L_{ω₁ω}-types (exists_small_model_of_hasArbLargeModels_countable_symbols).

The assembly keeps the identity of the local EM carrier throughout (it does NOT route through the existential tailTemplateRealizable_of_localEMContext_cross, which forgets it): a source model of size ≥ ℶ_{ω₁} feeds the schema term source (SchemaLocalEMSource.lean, the mixin-satisfying intermediate that itself realizes φ and carries the pairwise-distinct schemaSeq); over the highly order-transitive skeleton J of size κ (HighlyTransitiveExistence.lean) the schema context's carrier then has: satisfaction of φ (the stage-0 bridge realizes_stage0_sentence_of_skolemUniversal), size exactly max ℵ₀ κ = κ (mk_carrier_eq, injectivity from schemaSeq_pairwise_ne), and countably many realized types (lomega1omegaSmall on the localColim reduct, descended to the seed language by Lomega1omegaSmall.of_expansion).

theorem FirstOrder.Language.exists_small_model_of_hasArbLargeModels_countable_symbols {L' : Language} [Countable ((n : ℕ) × L'.Functions n)] [Countable ((n : ℕ) × L'.Relations n)] {φ : L'.Sentenceω} (hφarb : HasArbLargeModels φ) {κ : Cardinal.{0}} (hκ : Cardinal.aleph0 ≤ κ) : ∃ (N : Type) (x : L'.Structure N), φ.Realize N ∧ Cardinal.mk N = κ ∧ Lomega1omegaSmall N

The countable-symbol small-model theorem (Marker, Theorem 11.2 core): a sentence with arbitrarily large models has, at every infinite κ, a model of size exactly κ realizing only countably many complete L_{ω₁ω}-types.