Tail smallness bounds ranks on Cantor antichains

A countable-fragment alternative to uniform bounded back-and-forth comparison. The rank r is arbitrary: it need not be Borel and need not be an isomorphism invariant.

antichain_rank_bounded_of_fragment_tails: if for every countable sentence list θ there is a threshold b < ω₁ such that the spectrum of θ on the rank tail {c ∈ C | b ≤ r c} is countable, then r is bounded below ω₁ on every Borel Cantor isomorphism antichain in C. Recover the Cantor parameter by sentences (sentences_recover_cantor), so the parameters of high rank are countably many; the supremum of their successor ranks is a countable bound. The separating list is chosen after the antichain, so the tail hypothesis must hold for every list; the threshold may depend on the list.

fragment_tails_of_eventual_sentence_decision supplies that hypothesis from a stronger, sentence-by-sentence input: each sentence eventually has constant truth on the rank tail. Thresholds may depend on the whole sentence, not merely its quantifier rank.

sentenceTheory_image_countable_of_determining_cover is the named sentence-list specialization of the generic counting kernel Set.countable_image_of_determining_cover: a countable family of predicates on coded structures (not required to be formulas, Borel, invariant, or disjoint) that covers a set and determines the θ-theory on it makes the θ-spectrum of that set countable. Applied to a rank tail it supplies the tail hypothesis above; coverage and determination remain the producer's obligations.

ThinRankAnalysis.bounded_refined_of_fragment_tails discharges the refined boundedness field of ThinRankAnalysis with e := id: the bound holds on the whole antichain. The other fields of a thinness argument — countable ranks and countable fixed-rank antichains — remain inputs. Nothing here establishes tail smallness for any particular class.

Classical background

Scatteredness: Marker, Lectures on Infinitary Model Theory (Cambridge, 2016), Definition 3.3.1 and Corollary 3.3.10. The arbitrary-rank tail lemma is assembled here from the project's sentence-recovery API and does not occur in that form in the source.

theorem FirstOrder.Language.antichain_rank_bounded_of_fragment_tails {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (C : Set L.StructureSpace) (r : L.StructureSpace → Ordinal.{0}) (hr : ∀ c ∈ C, r c < Ordinal.omega 1) (htail : ∀ (θ : ℕ → L.Sentenceω), ∃ b < Ordinal.omega 1, (sentenceTheory θ '' {c : L.StructureSpace | c ∈ C ∧ b ≤ r c}).Countable) (f : (ℕ → Bool) → L.StructureSpace) (hf : Measurable f) (hm : ∀ (x : ℕ → Bool), f x ∈ C) (hanti : ∀ (x y : ℕ → Bool), x ≠ y → ¬L.structureIsoSetoid (f x) (f y)) : ∃ b < Ordinal.omega 1, ∀ (x : ℕ → Bool), r (f x) < b

Tail smallness bounds the rank on every Borel Cantor antichain, without a rank-domination theorem or a measurable rank.

theorem FirstOrder.Language.fragment_tails_of_eventual_sentence_decision {L : Language} [L.IsRelational] (C : Set L.StructureSpace) (r : L.StructureSpace → Ordinal.{0}) (hdecide : ∀ (θ : L.Sentenceω), ∃ b < Ordinal.omega 1, ∃ (p : Bool), ∀ c ∈ C, b ≤ r c → (c ∈ ModelsOf θ ↔ p = true)) (θ : ℕ → L.Sentenceω) : ∃ b < Ordinal.omega 1, (sentenceTheory θ '' {c : L.StructureSpace | c ∈ C ∧ b ≤ r c}).Countable

Eventual sentence decision gives tail smallness: if each sentence eventually has constant truth on the rank tail, every countable list has a countable tail spectrum. Countable suprema handle a whole list.

theorem FirstOrder.Language.sentenceTheory_image_countable_of_determining_cover {L : Language} [L.IsRelational] (θ : ℕ → L.Sentenceω) (C : Set L.StructureSpace) {E : Type u_1} [Countable E] (P : E → L.StructureSpace → Prop) (cover : ∀ c ∈ C, ∃ (e : E), P e c) (det : ∀ (e : E), ∀ c ∈ C, ∀ d ∈ C, P e c → P e d → sentenceTheory θ c = sentenceTheory θ d) : (sentenceTheory θ '' C).Countable

Countable sentence spectrum from a determining predicate cover. The sentence-list specialization of Set.countable_image_of_determining_cover: descriptions are arbitrary predicates P e on coded structures; if they cover C and any two members of C satisfying one description have the same θ-theory, the θ-spectrum of C is countable. No measurability, disjointness, invariance, selector, or symbol countability enters. With C a rank tail {c | c ∈ C ∧ b ≤ r c} this is the tail hypothesis of antichain_rank_bounded_of_fragment_tails for one list.

theorem FirstOrder.Language.ThinRankAnalysis.bounded_refined_of_fragment_tails {L : Language} [L.IsRelational] [Countable ((n : ℕ) × L.Relations n)] (C : Set L.StructureSpace) (r : L.StructureSpace → Ordinal.{0}) (hr : ∀ c ∈ C, r c < Ordinal.omega 1) (htail : ∀ (θ : ℕ → L.Sentenceω), ∃ b < Ordinal.omega 1, (sentenceTheory θ '' {c : L.StructureSpace | c ∈ C ∧ b ≤ r c}).Countable) (f : (ℕ → Bool) → L.StructureSpace) : Continuous f → (∀ (x : ℕ → Bool), f x ∈ C) → (∀ (x y : ℕ → Bool), x ≠ y → ¬L.structureIsoSetoid (f x) (f y)) → ∃ (e : (ℕ → Bool) → ℕ → Bool), Continuous e ∧ Function.Injective e ∧ ∃ β < Ordinal.omega 1, ∀ (x : ℕ → Bool), r (f (e x)) < β

The refined boundedness field from tail smallness, with e := id: the bound holds on the whole antichain, so no subcopy is needed. The remaining fields of ThinRankAnalysis are not supplied here.