The finite-tuple orbit bound

For the prefix specialization M := PrefixCarrier Bstar B A over lang U Lc, a conditional upper bound on orbit ranks and on the internal Scott rank, from:

• (H_sep) SepBounded and (H_up) UpwardClosed (DefaultLike …), the hypotheses of the row-profile bound;
• (H_orb) OrbitBounded: every tuple of every fiber has orbit rank below α, pointwise;
• component relationality and countability ([Lc.IsRelational], [Countable Bstar], [∀ u, Countable (B u)]); the carrier itself is not assumed countable;
• AddNatClosed α: closure below α under adding a finite ordinal on the right, supplied by any nonzero limit ordinal (AddNatClosed.of_isSuccLimit).

Theorem (exists_automorphism_bound): for every tuple a there is β < α such that every b with a ≡_β b is the image of a under an automorphism. The level is chosen from a before b: extend a by its owner rows (a⁺), fix a cover of a⁺, and let β₀ be the finite maximum of the profile bounds of the finitely many owner rows and the orbit ranks of the finitely many occupied fiber tuples; the witness is β₀ + n. Given b, the owner rows are added (bfEquiv_append_ownerRows, cost n), the owner block gives a compatible same-profile matching of rows extended to a profile-preserving permutation (exists_profilePerm), the level-0 atoms give the matching of the extended tuples along it (matched_of_sameAtomicType_ownerRows), and the fiber isomorphisms are adjusted to carry the extended tuple (exists_fiber_isos_carrying); the assembled automorphism restricts to a.

Corollary (internalScottRank_le_of_bounds): internalScottRank M ≤ α.

This is an upper bound under hypotheses; it is neither an exact rank nor a uniform orbit-determining level for all tuples.

Closure under finite addition

def FirstOrder.Language.FiberAssembly.AddNatClosed (α : Ordinal.{u}) : Prop

Closure below α under adding a finite ordinal on the right.

Equations

• FirstOrder.Language.FiberAssembly.AddNatClosed α = ∀ β < α, ∀ (n : ℕ), β + ↑n < α

theorem FirstOrder.Language.FiberAssembly.AddNatClosed.of_isSuccLimit {α : Ordinal.{u}} (h : Order.IsSuccLimit α) : AddNatClosed α

A nonzero limit ordinal is closed below under finite right addition.

The level-0 matching of owner-extended tuples

theorem FirstOrder.Language.FiberAssembly.matched_of_sameAtomicType_ownerRows {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] {n : ℕ} {a b : Fin n → Carrier R C} (e : R ≃ R) (h0 : SameAtomicType (Fin.append a (ownerRow a)) (Fin.append b (ownerRow b))) (he : ∀ (j : Fin n), e (owner (a j)) = owner (b j)) : Matched e (Fin.append a (ownerRow a)) (Fin.append b (ownerRow b))

Owner-extended tuples with the same atomic type are matched along any row bijection agreeing with the owner matching, in both directions and on both blocks.

theorem FirstOrder.Language.FiberAssembly.owners_present_append_ownerRows {U R : Type u} {C : R → Label U → Type u} {n : ℕ} (a : Fin n → Carrier R C) (i : Fin (n + n)) (r : R) (τ : Label U) : InFiber (Fin.append a (ownerRow a)) r τ i → ∃ (j : Fin (n + n)), Fin.append a (ownerRow a) j = Carrier.row r

In an owner-extended tuple every fiber point has its owner row present: only first-block coordinates are points, and their owners sit in the second block.

The orbit bound

def FirstOrder.Language.FiberAssembly.OrbitBounded {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

(H_orb) Pointwise component orbit bounds: every tuple of every fiber has orbit rank below α.

Equations

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

theorem FirstOrder.Language.FiberAssembly.exists_automorphism_bound {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 Bstar] [∀ (u : U), Countable (B u)] (α : Ordinal.{u}) (hsep : SepBounded Lc Bstar B A α) (hup : UpwardClosed (DefaultLike Lc Bstar B)) (horb : OrbitBounded Lc Bstar B A α) (hα : AddNatClosed α) (n : ℕ) (a : Fin n → PrefixCarrier Bstar B A) : ∃ β < α, ∀ (b : Fin n → PrefixCarrier Bstar B A), BFEquiv β n a b → ∃ (g : (lang U Lc).Equiv (PrefixCarrier Bstar B A) (PrefixCarrier Bstar B A)), ⇑g ∘ a = b

Finite-tuple orbit bound, pointwise automorphism form. For every tuple a there is β < α, chosen from a, such that every b with a ≡_β b is the image of a under an automorphism of the assembled structure.

theorem FirstOrder.Language.FiberAssembly.internalScottRank_le_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 Bstar] [∀ (u : U), Countable (B u)] (α : Ordinal.{u}) (hsep : SepBounded Lc Bstar B A α) (hup : UpwardClosed (DefaultLike Lc Bstar B)) (horb : OrbitBounded Lc Bstar B A α) (hα : AddNatClosed α) : internalScottRank (PrefixCarrier Bstar B A) ≤ α

Internal Scott rank bound. Under the same hypotheses, the internal Scott rank of the assembled structure is at most α.