Analytic subsets of the well-order class are bounded (issue #64)

Boundedness for analytic families of coded well-orders: if A is an analytic set of codes, every one of which interprets the distinguished relation as a well-order, then a single countable ordinal bounds all their order types.

The classical statement is the boundedness theorem for Σ¹₁ subsets of WO; here it is obtained through the project's López–Escobar machinery rather than through a rank analysis, by routing an analytic A into a single L_{ω₁ω} sentence and then invoking Marker's Corollary 4.4.2 (Marker, Lectures on Infinitary Model Theory, Cambridge, 2016; Corollary 4.27 of the 2013 notes). Compare Gao, Invariant Descriptive Set Theory (CRC Press, 2009), Theorem 1.6.10.

The route

1. exists_tree_of_analyticSet puts A in tree normal form: A is the branch projection of a level-indexed cylinder tree T along the query code.
2. pcSentence L .left T is a sentence Θ over the expanded language L' := graphLanguage (KLang L), and the PC gates sandwich its reduct class: A ⊆ codeReduct '' ModelsOf Θ ⊆ W for every isomorphism-invariant W ⊇ A.
3. Taking W := wellOrderClass lt — invariant by wellOrderClass_isomorphismInvariant, and a superset of A by hypothesis — the upper gate says exactly that every model of Θ is a well-order for the transported relation GraphRelation.base (Sum.inl lt). No transport lemma is needed: codeReduct_toStructure is Iff.rfl, so the two memberships are the same proposition.
4. isWellOrder_of_realize_of_modelsOf_subset — the containment form of the defect bridge, which exists for this consumer — lifts that from codes to arbitrary models of Θ ⊓ infiniteAxiom.
5. wellOrder_type_boundedness bounds all of those order types by one countable β.
6. The lower gate subset_pcClass exhibits each c ∈ A as codeReduct d for a model d of Θ, and ℕ is infinite, so the bound applies to d — and lands on c definitionally.

Why the arbitrary-language endpoint. Step 5 uses wellOrder_type_boundedness, not wellOrder_type_boundedness_relational. The expanded language L' carries a graph relation for every function symbol of KLang L, and asserting a Countable (Σ l, L'.Relations l) instance here would re-derive exactly what Methods/WellOrdering/GraphTranslation.lean was written to remove. The public endpoint has no symbol-countability hypothesis; the relationalization is already inside it.

theorem FirstOrder.Language.analytic_wellOrder_type_boundedness {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {A : Set L.StructureSpace} (lt : L.Relations 2) (hA : MeasureTheory.AnalyticSet A) (hAW : A ⊆ wellOrderClass lt) : ∃ α < (Cardinal.aleph 1).ord, ∀ c ∈ A, ∀ (h : IsWellOrder ℕ fun (x y : ℕ) => Structure.RelMap lt ![x, y]), (Ordinal.type fun (x y : ℕ) => Structure.RelMap lt ![x, y]) < α

Boundedness for analytic families of coded well-orders (issue #64): if every code in an analytic set A interprets lt as a well-order, then a single countable ordinal α strictly bounds every one of their order types.

The class A itself need not be isomorphism-invariant — only the envelope wellOrderClass lt is, which is what the sandwich A ⊆ codeReduct '' ModelsOf Θ ⊆ wellOrderClass lt consumes.

Pullback along a continuous coding

Boundedness is usually consumed one step removed: an analytic set B in some other space carries a continuous assignment of well-order codes, and what needs bounding is a rank read off those codes. The image code '' B is analytic, sits inside wellOrderClass lt, and the bound transports back.

theorem FirstOrder.Language.analytic_rank_bounded_of_continuousOn_wellOrderPresentation_le {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {X : Type u_1} [TopologicalSpace X] {B : Set X} (lt : L.Relations 2) (hB : MeasureTheory.AnalyticSet B) (code : X → L.StructureSpace) (hcode : ContinuousOn code B) (hWO : ∀ x ∈ B, code x ∈ wellOrderClass lt) (rank : X → Ordinal.{0}) (hrank : ∀ x ∈ B, ∀ (h : IsWellOrder ℕ fun (a b : ℕ) => Structure.RelMap lt ![a, b]), rank x ≤ Ordinal.type fun (a b : ℕ) => Structure.RelMap lt ![a, b]) : ∃ β < (Cardinal.aleph 1).ord, ∀ x ∈ B, rank x < β

Boundedness along a continuous well-order presentation, ≤-form: if an analytic B maps continuously to codes that are all well-orders, and the presented well-order dominates rank, then one countable ordinal bounds rank on B.

hrank is stated for every well-ordering proof, so the hypothesis never mentions a particular IsWellOrder term — the caller supplies whichever one it has.

theorem FirstOrder.Language.analytic_rank_bounded_of_continuousOn_wellOrderPresentation {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {X : Type u_1} [TopologicalSpace X] {B : Set X} (lt : L.Relations 2) (hB : MeasureTheory.AnalyticSet B) (code : X → L.StructureSpace) (hcode : ContinuousOn code B) (hWO : ∀ x ∈ B, code x ∈ wellOrderClass lt) (rank : X → Ordinal.{0}) (hrank : ∀ x ∈ B, ∀ (h : IsWellOrder ℕ fun (a b : ℕ) => Structure.RelMap lt ![a, b]), rank x = Ordinal.type fun (a b : ℕ) => Structure.RelMap lt ![a, b]) : ∃ β < (Cardinal.aleph 1).ord, ∀ x ∈ B, rank x < β

Boundedness along a continuous well-order presentation: the equality form, where rank computes the order type of the presented code. The ≤-form above is the implementation.

The regression: the full well-order class is not analytic

The A := wellOrderClass lt case. Were the class analytic it would bound its own order types, but it realizes every countably infinite one — α + ω in particular.

theorem FirstOrder.Language.wellOrderClass_not_analyticSet {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (lt : L.Relations 2) : ¬MeasureTheory.AnalyticSet (wellOrderClass lt)

The countable well-order class is not analytic: no analytic set of codes consists exactly of the well-ordered ones. Non-Borelness (wellOrderClass_not_measurableSet) is weaker, since Borel sets are analytic; that endpoint is proved separately from López–Escobar and does not go through this one.