Countable: model existence + model theory for countable structures

Import this bundle for the Henkin construction, model existence theorem, Löwenheim-Skolem, Hanf numbers, counting models, and the EM-stretching chain (indiscernibles → templates → realization).

The _of_compact endpoints (Methods/EM/FragmentAdapter.lean and the tail variants in TailAdapter.lean) are part of this bundle. They take a Theoryω.OrdinaryCompactness oracle as a hypothesis and mention no admissible notion, so import InfinitaryLogic.Countable remains admissible-free.