Admissible: admissible fragments, conditional compactness interfaces, proof system

Import this bundle for the admissible-fragment interface, the conditional compactness interfaces (both the project's HF-style axiom and the literature-faithful interface), proof system / derivability, soundness, and the consistency-property bridge. The EM adapter theorems (Methods/EM/FragmentAdapter.lean and the tail-indiscernibility variants in Methods/EM/TailAdapter.lean) live here rather than in Countable, keeping that bundle admissible-free.