Descriptive: descriptive set theory of Lω₁ω model classes

Import this bundle for the structure space, satisfaction measurability, Borel complexity, counting dichotomy, finite carrier analysis, and the countable-model counting theorems.

It also provides reusable DST infrastructure, developed for the proof of Silver's theorem. Everything below is generic — pure Mathlib imports, no model theory — except StructureIsoSetoid, which is deliberately the model-theoretic application of that vocabulary:

• CantorAntichain: Cantor-scheme → perfect-antichain extraction (CantorScheme.exists_antichain_map and the splitting-predicate builder);
• PerfectAntichain: perfect/Cantor-antichain and thinness vocabulary, plus the perfect-set and Polish-quotient cardinal facts
• StructureIsoSetoid: the application — isomorphism defined once on the ambient StructureSpace L, isoSetoid φ as its restriction, and the sentence-level perfect-set/thinness predicates stated against it
• RankedThinness: the countable-ordinal rank route to thinness (ThinRankAnalysis), with the quotient-countability step (Setoid.countable_antichain);
• BorelFunctionalGraph: Borel graphs with singleton vertical sections — Borel domain, measurable-embedding projection, and the induced measurable partial function, all via Lusin–Souslin;
• Mycielski: Mycielski's theorem for Cantor space (mycielski_cantor);
• CantorStabilization: countably many Borel-fibred maps on Cantor space are simultaneously continuous along one continuous injective Cantor subcopy (CantorStabilization.exists_subcopy_continuous), with the Borel-set form of the Cantor-copy extraction (MeasurableSet.exists_nat_bool_injection_of_not_countable);
• KleeneBrouwer: the Kleene–Brouwer order on a tree over ℕ — no infinite branch is well-foundedness of strict extension, KB is a well-order on a well-founded tree (KleeneBrouwer.isWellOrder_kbLT), and the tree height is bounded by the KB order type (KleeneBrouwer.treeHeight_le_type);
• TreeCodes: tree codes over a countable alphabet, the closed tree class, the continuous Kleene–Brouwer code into Language.order, and analytic boundedness for well-founded trees (analytic_wellFoundedTree_rank_boundedness) with its domination adapter;
• KuratowskiUlam: the meager-sections direction of Kuratowski–Ulam (isMeagre_of_isMeagre_sections);
• GSGraph: the graphs G_S(2^ℕ) and Miller's independence lemma (exists_gSGraph_edge_of_not_isMeagre);
• G0Dichotomy: the KST independent-superset lemma (exists_measurableSet_relIndependent_superset) and the positivity ideals (SmallFam) with the combination lemma (not_smallFam_comb_cross);
• G0Fusion: the fusion recursion and limit (G0Fusion.exists_gsGraph_hom), the classical G₀-dichotomy construction.

Note: the Silver chain (Silver-Burgess, the category route, and Gandy-Harrington — all sorry-free) lives in InfinitaryLogic.Conditional. The model-theoretic counting modules imported above depend on descriptive results and are included here.