The row-profile bound

For the prefix specialization (rows are allowed words, the fiber at (r, τ) is the component B (last τ) when τ ⪯ r and the default B_* otherwise), the profile of a row is the label-indexed family of isomorphism types of its fibers.

• DefaultLike Lc Bstar B u: the component B u is isomorphic to the default.
• SepBounded Lc Bstar B A α (H_sep): for every N some level β_N < α separates, from the default, every non-default-like component at a position n ≤ N.
• (H_up) is UpwardClosed (DefaultLike Lc Bstar B): default-like components are upward closed.

Theorem (exists_profile_bound): under (H_sep) and (H_up), for every row r there is β < α such that every row s with row r ≡_β row s in the assembled structure has fibers isomorphic to those of r at every label.

The proof takes β := β_{r.length}. Restriction (bfEquiv_restrict_nil) gives C(r, τ) ≡_β C(s, τ) for every label. If the non-default prefix sets of r and s differed, finite-prefix detection would produce a non-default label of length at most r.length + 1, hence ending at a position at most r.length, prefixing exactly one row; its fiber is a non-default-like component on one side and the default on the other, and the letter is allowed at that position by whichever row it prefixes, contradicting (H_sep). With equal non-default prefix sets the fibers are isomorphic label by label (prefixFiber_equiv_of_ndPrefixes_eq): shared or absent prefixes give literally equal components, and a prefix of one row only carries a default-like component.

Neither countability nor relationality is needed; DefaultLike supplies the isomorphism witnesses. Nesting, limit assumptions on α, and orbit hypotheses do not enter.

def FirstOrder.Language.FiberAssembly.DefaultLike {U : Type u} (Lc : Language) (Bstar : Type u) (B : U → Type u) [Lc.Structure Bstar] [(u : U) → Lc.Structure (B u)] (u : U) : Prop

A component is default-like when it is isomorphic to the default component.

Equations

• FirstOrder.Language.FiberAssembly.DefaultLike Lc Bstar B u = Nonempty (Lc.Equiv (B u) Bstar)

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

(H_sep) Separation at bounded positions: for every N some level β_N < α separates every non-default-like component at a position n ≤ N from the default.

Equations

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

Transport along component indices

theorem FirstOrder.Language.FiberAssembly.last_mem_of_prefix {U : Type u} [LinearOrder U] {A : ℕ → Set U} {p : Row A} {τ : Label U} (h : ↑τ <+: ↑p) : τ.last ∈ A ((↑τ).length - 1)

The last letter of a prefix of an allowed row is allowed at the prefix's last position.

Equal non-default prefix sets give isomorphic fibers

theorem FirstOrder.Language.FiberAssembly.prefixFiber_equiv_of_ndPrefixes_eq {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} {r s : Row A} (hnd : ndPrefixes (DefaultLike Lc Bstar B) ↑r = ndPrefixes (DefaultLike Lc Bstar B) ↑s) (τ : Label U) : Nonempty (Lc.Equiv (prefixFiber Bstar B A r τ) (prefixFiber Bstar B A s τ))

Rows with the same non-default prefixes have isomorphic fibers at every label: shared or absent prefixes give literally equal components, and a prefix of one row only carries a default-like component.

The profile bound

theorem FirstOrder.Language.FiberAssembly.exists_profile_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} (α : Ordinal.{u_1}) (hsep : SepBounded Lc Bstar B A α) (hup : UpwardClosed (DefaultLike Lc Bstar B)) (r : Row A) : ∃ β < α, ∀ (s : Row A), BFEquiv β 1 ![Carrier.row r] ![Carrier.row s] → ∀ (τ : Label U), Nonempty (Lc.Equiv (prefixFiber Bstar B A r τ) (prefixFiber Bstar B A s τ))

Row-profile bound, pointwise form. Under (H_sep) and (H_up), for every row r there is β < α such that any row s with row r ≡_β row s has fibers isomorphic to those of r at every label.