The exact internal Scott rank, conditionally

The upper bound internalScottRank_le_of_bounds combined with the two-row lower bound of FiberTwoRow.

• CofinalApprox: below every level β < α some nonempty allowed row ends in a letter whose component is β-equivalent to the default (empty tuples) but not isomorphic to it. The row is part of the hypothesis: nesting alone does not produce an allowed row ending in a given allowed letter. This is consistent with (H_sep): separation levels bound only positions up to N, so the approximating rows end at positions growing with β.
• le_internalScottRank_of_cofinalApprox: under nesting and cofinal approximation, the internal Scott rank is at least α. The two-row pair row p, row (concatRow p) is β-equivalent (twoRow_bfEquiv) but not automorphic (twoRow_not_automorphic). The lower bound goes through the orbit-rank automorphism criterion on the assembled structure, so the carrier must be countable: [Countable U] is assumed in addition to component countability, and rows and carrier are then countable by the existing instances. The upper bound alone does not need this.
• internalScottRank_eq_of_bounds: le_antisymm of the upper and lower bounds.

The result is conditional on all the listed hypotheses; no concrete exact-rank instance is supplied here.

def FirstOrder.Language.FiberAssembly.CofinalApprox {U : Type u} [LinearOrder U] (Lc : Language) (Bstar : Type u) (B : U → Type u) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] (A : ℕ → Set U) (α : Ordinal.{u}) : Prop

Cofinal approximation by allowed rows. Below every level β < α some nonempty allowed row ends in a letter whose component is β-equivalent to the default (empty tuples) but not isomorphic to it.

Equations

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

theorem FirstOrder.Language.FiberAssembly.le_internalScottRank_of_cofinalApprox {U : Type u} [LinearOrder U] {Lc : Language} {Bstar : Type u} {B : U → Type u} [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] {A : ℕ → Set U} [Lc.IsRelational] [Countable U] [Countable Bstar] [∀ (u : U), Countable (B u)] (hA : Nested A) (α : Ordinal.{u}) (hcof : CofinalApprox Lc Bstar B A α) : α ≤ internalScottRank (PrefixCarrier Bstar B A)

Lower bound. Under nesting and cofinal approximation, in the (countable) assembled structure the internal Scott rank is at least α.

theorem FirstOrder.Language.FiberAssembly.internalScottRank_eq_of_bounds {U : Type u} [LinearOrder U] {Lc : Language} {Bstar : Type u} {B : U → Type u} [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] {A : ℕ → Set U} [Lc.IsRelational] [Countable U] [Countable Bstar] [∀ (u : U), Countable (B u)] (hA : Nested A) (α : Ordinal.{u}) (hsep : SepBounded Lc Bstar B A α) (hup : UpwardClosed (DefaultLike Lc Bstar B)) (horb : OrbitBounded Lc Bstar B A α) (hα : AddNatClosed α) (hcof : CofinalApprox Lc Bstar B A α) : internalScottRank (PrefixCarrier Bstar B A) = α

Exact internal Scott rank, conditionally: the upper bound of FiberOrbitBound and the lower bound above.