Adapter C: counting successor-level classes from types and extension spectra

countable_bfTupleQuotient_succ counts the (α+1)-classes of n-tuples of a class of coded models from two inputs: countably many depth-α classes of n-tuples, and countably many realized depth-α extension spectra (each a set of classes of (n+1)-tuples). Countably many extension classes do not give countably many sets of them, so the two inputs are supplied separately and never conflated:

• Input 1 from fragment types, through adapter B. If the bounded Scott formula of every tuple at level α belongs to F, then equal F-types force depth-α equivalence, so a countable realized F-type spectrum gives countably many depth-α classes (countable_bfTupleQuotient_of_types). This uses B (fragment types refine BFEquiv α), not A.
• Input 2 from a determining cover on the spectrum map. A countable family of descriptions covering the tuples, any two tuples sharing a description having the same whole extension spectrum, gives countably many realized spectra (countable_bfExtensionSpectra_of_cover), by Set.countable_image_of_determining_cover applied directly to bfExtensionSpectrum.

countable_bfTupleQuotient_succ_of_types_and_cover feeds both to the existing successor theorem; its conclusion is at Order.succ α, the successor visible. The characterization bfTupleSetoid_succ_iff (α-equivalence together with equal depth-α spectra) is used as is.

theorem FirstOrder.Language.countable_quotient_of_countable_range {X : Type u_1} {T : Type u_2} (s : Setoid X) (t : X → T) (hrange : (Set.range t).Countable) (h : ∀ (x y : X), t x = t y → s x y) : Countable (Quotient s)

A quotient is countable when a map with countable range refines the relation: fibres of the map lie inside classes. The proof chooses one preimage for each value in the range (classical choice; not a Borel selector and not a choice of canonical structures).

theorem FirstOrder.Language.Fragment.range_pointedType_subset_typeSpectrum {L : Language} [L.IsRelational] (F : L.Fragment) (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (n : ℕ) : (Set.range fun (x : CodedModelTuple φ C n) => F.pointedType (↑↑x.1) x.2) ⊆ F.typeSpectrum n (Subtype.val '' C)

The realized F-types of the n-tuples of C-models lie in the spectrum of F on the underlying codes.

theorem FirstOrder.Language.Fragment.countable_bfTupleQuotient_of_types {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (F : L.Fragment) (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) (hα : α < Ordinal.omega 1) (hmem : ∀ (x : CodedModelTuple φ C n), ⟨n, scottBounded x.2 α⟩ ∈ F) (htypes : (F.typeSpectrum n (Subtype.val '' C)).Countable) : Countable (Quotient (bfTupleSetoid φ C α n))

Input 1, from fragment types through adapter B. If the bounded Scott formula at level α < ω₁ of every n-tuple of a C-model belongs to F, and F realizes countably many n-types on the codes of C, then there are countably many depth-α classes of n-tuples.

theorem FirstOrder.Language.Fragment.countable_bfExtensionSpectra_of_cover {L : Language} [L.IsRelational] (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) {E : Type u_1} [Countable E] (P : E → CodedModelTuple φ C n → Prop) (cover : ∀ (x : CodedModelTuple φ C n), ∃ (e : E), P e x) (det : ∀ (e : E) (x y : CodedModelTuple φ C n), P e x → P e y → bfExtensionSpectrum φ C α n x = bfExtensionSpectrum φ C α n y) : Countable ↑(bfExtensionSpectra φ C α n)

Input 2, from a determining cover on the spectrum map. Countably many descriptions cover the n-tuples of C-models, and any two tuples sharing a description have the same depth-α extension spectrum; then countably many spectra are realized. Determination is equality of whole spectra, not of extension classes.

theorem FirstOrder.Language.Fragment.countable_bfTupleQuotient_succ_of_types_and_cover {L : Language} [L.IsRelational] [Countable ((l : ℕ) × L.Relations l)] (F : L.Fragment) (φ : L.Sentenceω) (C : Set ↑(ModelsOf φ)) (α : Ordinal.{0}) (n : ℕ) (hα : α < Ordinal.omega 1) (hmem : ∀ (x : CodedModelTuple φ C n), ⟨n, scottBounded x.2 α⟩ ∈ F) (htypes : (F.typeSpectrum n (Subtype.val '' C)).Countable) {E : Type u_1} [Countable E] (P : E → CodedModelTuple φ C n → Prop) (cover : ∀ (x : CodedModelTuple φ C n), ∃ (e : E), P e x) (det : ∀ (e : E) (x y : CodedModelTuple φ C n), P e x → P e y → bfExtensionSpectrum φ C α n x = bfExtensionSpectrum φ C α n y) : Countable (Quotient (bfTupleSetoid φ C (Order.succ α) n))

Adapter C. Both counting inputs, then the existing successor theorem: countably many (α+1)-classes of n-tuples. The successor is visible in the conclusion.