Ranked thinness from well-order presentations (issue #64)

The adapter between analytic boundedness and the thinness package: a rank that is computed by coded well-orders, presented continuously on each Cantor antichain, satisfies ThinRankAnalysis's bounded-on-Cantor-antichains field.

The quantifier order is the content

The presentation is supplied inside the antichain callback, and only on a Cantor subcopy:

∀ f, Continuous f → … → ∃ e, Continuous e ∧ Injective e ∧
                          ∃ code : (ℕ → Bool) → StructureSpace L, …

not as a global X → StructureSpace L field. Each Cantor antichain gets to choose its own coding, and need only present a subcopy of itself. A global presentation would impose an unwanted global rank bound and is stronger than intended consumers can supply; requiring the whole antichain to be presented is likewise stronger than the thinness argument needs, since that argument runs on any Cantor subcopy. Producing the per-antichain presentation is the hard downstream mathematics; boundedness itself, once a presentation exists, is this file.

ThinRankAnalysis.of_full_wellOrderPresentations recovers the whole-antichain form for producers that have it, by taking the subcopy to be the identity. Only that direction is supplied; no converse is claimed.

The boundedness field is then four lines: the antichain's coding domain is all of Cantor space, which is analytic because it is closed in a Polish space, so analytic_rank_bounded_of_continuousOn_wellOrderPresentation applies at B := Set.univ.

ThinRankAnalysis measures against Ordinal.omega 1 and the boundedness layer against (Cardinal.aleph 1).ord; Cardinal.ord_aleph identifies them.

def FirstOrder.Language.ThinRankAnalysis.of_wellOrderPresentations {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {X : Type w} [TopologicalSpace X] {r : Setoid X} {A : Set X} (lt : L.Relations 2) (rank : X → Ordinal.{0}) (rank_lt_omega1 : ∀ x ∈ A, rank x < Ordinal.omega 1) (fixedRankAntichains_countable : ∀ α < Ordinal.omega 1, ∀ B ⊆ A, (∀ x ∈ B, rank x = α) → (∀ x ∈ B, ∀ y ∈ B, r x y → x = y) → B.Countable) (present : ∀ (f : (ℕ → Bool) → X), Continuous f → (∀ (x : ℕ → Bool), f x ∈ A) → (∀ (x y : ℕ → Bool), x ≠ y → ¬r (f x) (f y)) → ∃ (e : (ℕ → Bool) → ℕ → Bool), Continuous e ∧ Function.Injective e ∧ ∃ (code : (ℕ → Bool) → L.StructureSpace), Continuous code ∧ (∀ (x : ℕ → Bool), code x ∈ wellOrderClass lt) ∧ ∀ (x : ℕ → Bool) (h : IsWellOrder ℕ fun (a b : ℕ) => Structure.RelMap lt ![a, b]), rank (f (e x)) = Ordinal.type fun (a b : ℕ) => Structure.RelMap lt ![a, b]) : ThinRankAnalysis r A

Ranked thinness from per-antichain well-order presentations: a rank whose value on each continuous Cantor antichain is realized as the order type of a continuously-presented family of coded well-orders is a ThinRankAnalysis.

The first two hypotheses are ThinRankAnalysis's own fields, passed through unchanged. Only bounded_on_refined_cantor_antichains is derived, and present is exactly what it needs: given an antichain f, a Cantor subcopy e together with a continuous coding of Cantor space by well-orders whose order types are the ranks along f ∘ e.

ThinRankAnalysis is evidence, not a proposition, so this is a def.

Equations

• One or more equations did not get rendered due to their size.

def FirstOrder.Language.ThinRankAnalysis.of_full_wellOrderPresentations {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] {X : Type w} [TopologicalSpace X] {r : Setoid X} {A : Set X} (lt : L.Relations 2) (rank : X → Ordinal.{0}) (rank_lt_omega1 : ∀ x ∈ A, rank x < Ordinal.omega 1) (fixedRankAntichains_countable : ∀ α < Ordinal.omega 1, ∀ B ⊆ A, (∀ x ∈ B, rank x = α) → (∀ x ∈ B, ∀ y ∈ B, r x y → x = y) → B.Countable) (present : ∀ (f : (ℕ → Bool) → X), Continuous f → (∀ (x : ℕ → Bool), f x ∈ A) → (∀ (x y : ℕ → Bool), x ≠ y → ¬r (f x) (f y)) → ∃ (code : (ℕ → Bool) → L.StructureSpace), Continuous code ∧ (∀ (x : ℕ → Bool), code x ∈ wellOrderClass lt) ∧ ∀ (x : ℕ → Bool) (h : IsWellOrder ℕ fun (a b : ℕ) => Structure.RelMap lt ![a, b]), rank (f x) = Ordinal.type fun (a b : ℕ) => Structure.RelMap lt ![a, b]) : ThinRankAnalysis r A

Compatibility with a presentation of the whole antichain. A producer that can present every point of a Cantor antichain — the stronger, older hypothesis — still yields a ThinRankAnalysis: take the subcopy to be the identity.

Delegates to ThinRankAnalysis.of_wellOrderPresentations; the analytic-boundedness argument lives there and is not repeated. Only this direction is supplied, and no converse is claimed.

Equations

• One or more equations did not get rendered due to their size.

Regression: the former hypotheses still construct an analysis