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 admissible-fragment adapter theorems (_of_fragment, _of_fullFragment, _of_compact) are in Methods/EM/FragmentAdapter.lean, imported by the Admissible bundle — NOT by this bundle. So import InfinitaryLogic.Countable is genuinely countable-side only.