Genuine downward Löwenheim–Skolem for fragments (issue #13 unit 5)

Per the frozen audit (docs/fragments-audit.md §5–§6): from an arbitrary M and X ⊆ M, construct an A-elementary substructure containing X with the HONEST cardinal bound

|N| ≤ max(ℵ₀, |X|, |A|, |Σ n, L.Functions n|).

The construction is the semantic witness hull (Marker, Exercise 1.23, presented with choice functions instead of a language expansion): interleave Substructure.closure (all language functions — this is where |Σ Functions| honestly enters) with chosen witnesses for failures of the fragment-controlled universals (tvWitnessSet — |A|-many witness suppliers), iterate ω times, and close once more. The union is closed under both, so the Tarski–Vaught criterion (aElementary_of_tarskiVaught) applies. Witnesses are extracted from existence proofs (Exists.choose), so no Nonempty M hypothesis and no dummy elements are needed.

Marker's textbook bound max(|A|,|X|) (Theorem 1.22) is the special case |Σ Functions| ≤ max ℵ₀ |A|; the countable corollary, which is what the consumers use, is exists_countable_aElementary_substructure.

The language's two universes and the carrier's are independent. The three cardinals being compared therefore start in three different universes, so every bound is stated with an explicit Cardinal.lift into max u v w. exists_aElementary_substructure_of_eq_univ is the same-universe form, where those lifts are identities.

The witness sets and the hull

The cardinal bound

Mathlib's heterogeneous-universe lemmas produce the complementary lift level: for a set in M they give lift.{max u v}, and for language-side data lift.{w}. Both land in Cardinal.{max u v w}, but Lean keeps the level expressions distinct, so every bound below is stated with the uniform lift.{max u v w} and converted once through these.

theorem FirstOrder.Language.exists_countable_aElementary_substructure {L : Language} {M : Type w} [L.Structure M] (A : L.Fragment) {X : Set M} (hX : X.Countable) (hA : A.toSet.Countable) [hF : Countable ((n : ℕ) × L.Functions n)] : ∃ (N : L.Substructure M), X ⊆ ↑N ∧ AElementary A N.subtype ∧ Countable ↥N

The countable corollary (Marker, Theorem 1.22 second half — what #17 consumes): countable data yields a countable A-elementary substructure.

Universe regression

These instantiate the hull construction and its cardinal bound where the language's two universes and the structure's universe are pairwise distinct, and at the same-universe specialization. They are compiled, so they fail if the file is ever reconstrained; the variable block alone would not catch that, since a Language.{u, v} binder can still be silently pinned by a downstream lemma.