López–Escobar, hard direction (issue #10, Unit 5b)

The endpoint: every invariant Borel class of countable L-structures is the model class of a single L_ω₁ω-sentence.

The assembly is Marker's, with every ingredient already proved:

1. B and Bᶜ are analytic, so Unit 0 (exists_tree_of_analyticSet) presents each by a cylinder tree — T₀ for B, T₁ for Bᶜ;
2. Unit 4 (pcSentences_entails_not) says the two PC sentences have no common model;
3. Craig separation (craig_pcSeparation_relational, issue #8) separates them by a sentence θ₀ of their shared vocabulary;
4. Unit 5a (sharedToBase, realize_sharedToBase) decodes θ₀ into an L-sentence and transports its truth to base codes;
5. both inclusions then use only the invariance-free forward presentation subset_pcClass (Unit 3a) — one side for B, the other for Bᶜ.

So IsomorphismInvariant is consumed exactly where Unit 3b/Unit 4 already consumed it, inside pcSentences_entails_not; this unit adds no further use of it.

theorem FirstOrder.Language.lopez_escobar {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {B : Set L.StructureSpace} (hB : MeasurableSet B) (hinv : IsomorphismInvariant B) : ∃ (φ : L.Sentenceω), B = ModelsOf φ

López–Escobar, hard direction: an isomorphism-invariant Borel class of coded countable L-structures is the model class of a single L_ω₁ω-sentence.