The two-row lower bound in the prefix specialization

In the prefix specialization (PrefixCarrier B_* B A), take a nonempty allowed row p ending in the letter u, and the row q = p ++ [u] obtained by repeating that last letter. Under the nesting hypothesis A n ⊆ A (n + 1), q is again an allowed row (isAllowed_concat_last). The fibers of p and q agree at every label except q itself (compIndex_concat_last_of_ne), where p carries the default component B_* and q carries B u (compIndex_concat_last_self, compIndex_of_not_prefix).

Two-row lower bound (twoRow_bfEquiv, twoRow_not_automorphic): if B u and B_* are back-and-forth equivalent at level β as structures (the empty tuples), the two row elements are BFEquiv β in the assembled language, through the fixed transposition of p and q and the generic assembly theorem; and if B u ≇ B_*, no automorphism carries the row p to the row q, by restricting a putative one to the differing fiber (restrictFiber, which is where relationality of Lc enters). Neither statement needs countability.

Orbit-rank corollary (twoRow_lt_orbitRank), stated separately: for a countable assembled structure, the orbit rank of the row p exceeds β. This is the only place the orbit characterization, hence countability, is used.

A row-tuple corollary of the generic assembly theorem is supplied on the way (fiberBF_of_no_points): a tuple with no fiber points needs only the empty-tuple data of every fiber.

No cofinal-rank assembly, full-profile bound, or companion construction appears here.

Repeating the last letter of an allowed row

theorem FirstOrder.Language.FiberAssembly.le_getLast_of_pairwise {U : Type u} [LinearOrder U] {p : List U} (hp : List.Pairwise (fun (x1 x2 : U) => x1 ≤ x2) p) (hne : p ≠ []) {a : U} (ha : a ∈ p) : a ≤ p.getLast hne

Every letter of a nondecreasing list is at most its last letter.

def FirstOrder.Language.FiberAssembly.Nested {U : Type u} (A : ℕ → Set U) : Prop

Nesting of the allowed sets: each level's allowed letters remain allowed at the next.

Equations

• FirstOrder.Language.FiberAssembly.Nested A = ∀ (n : ℕ), A n ⊆ A (n + 1)

theorem FirstOrder.Language.FiberAssembly.isAllowed_concat_last {U : Type u} [LinearOrder U] {A : ℕ → Set U} (hA : Nested A) {p : List U} (hp : IsAllowed A p) (hne : p ≠ []) : IsAllowed A (p ++ [p.getLast hne])

Under nesting, repeating the last letter of a nonempty allowed row gives an allowed row.

The fibers of p and q = p ++ [u]

def FirstOrder.Language.FiberAssembly.concatLabel {U : Type u} (p : List U) (u : U) : Label U

The label q = p ++ [u] itself.

Equations

• FirstOrder.Language.FiberAssembly.concatLabel p u = ⟨p ++ [u], ⋯⟩

theorem FirstOrder.Language.FiberAssembly.concatLabel_last {U : Type u} (p : List U) (u : U) : (concatLabel p u).last = u

theorem FirstOrder.Language.FiberAssembly.compIndex_concat_last_of_ne {U : Type u} [LinearOrder U] (p : List U) (u : U) (τ : Label U) (hτ : τ ≠ concatLabel p u) : compIndex (p ++ [u]) τ = compIndex p τ

Away from the label q, the fibers of p and q are indexed alike.

theorem FirstOrder.Language.FiberAssembly.compIndex_concat_last_self {U : Type u} [LinearOrder U] (p : List U) (u : U) : compIndex (p ++ [u]) (concatLabel p u) = some u

At the label q, the fiber of q is the component B u.

theorem FirstOrder.Language.FiberAssembly.compIndex_concat_label_of_shorter {U : Type u} [LinearOrder U] (p : List U) (u : U) : compIndex p (concatLabel p u) = none

At the label q, the fiber of p is the default component.

A row-tuple corollary of the generic assembly theorem

theorem FirstOrder.Language.FiberAssembly.fiberBF_of_no_points {U : Type u} {Lc : Language} {R S : Type u} {C : R → Label U → Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] {e : R ≃ S} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (hm : Matched e a b) (hno : ∀ (i : Fin n) (r : R) (τ : Label U), ¬InFiber a r τ i) {α : Ordinal.{u_1}} (h0 : ∀ (r : R) (τ : Label U), BFEquiv α 0 Fin.elim0 Fin.elim0) : FiberBF Lc α e hm

A tuple with no fiber points needs only the empty-tuple data of every fiber.

The two rows

@[instance_reducible]

instance FirstOrder.Language.FiberAssembly.instDecidableEqRow {U : Type u} [LinearOrder U] {A : ℕ → Set U} : DecidableEq (Row A)

Equations

• FirstOrder.Language.FiberAssembly.instDecidableEqRow = FirstOrder.Language.FiberAssembly.instDecidableEqRow._aux_1

def FirstOrder.Language.FiberAssembly.concatRow {U : Type u} [LinearOrder U] {A : ℕ → Set U} (hA : Nested A) (p : Row A) (hne : ↑p ≠ []) : Row A

The row q = p ++ [u], allowed under nesting.

Equations

• FirstOrder.Language.FiberAssembly.concatRow hA p hne = ⟨↑p ++ [(↑p).getLast hne], ⋯⟩

theorem FirstOrder.Language.FiberAssembly.concatRow_ne {U : Type u} [LinearOrder U] {A : ℕ → Set U} (hA : Nested A) (p : Row A) (hne : ↑p ≠ []) : concatRow hA p hne ≠ p

def FirstOrder.Language.FiberAssembly.twoRowSwap {U : Type u} [LinearOrder U] {A : ℕ → Set U} (hA : Nested A) (p : Row A) (hne : ↑p ≠ []) : Row A ≃ Row A

The fixed transposition of the two rows.

Equations

• FirstOrder.Language.FiberAssembly.twoRowSwap hA p hne = Equiv.swap p (FirstOrder.Language.FiberAssembly.concatRow hA p hne)

theorem FirstOrder.Language.FiberAssembly.twoRowSwap_apply_left {U : Type u} [LinearOrder U] {A : ℕ → Set U} (hA : Nested A) (p : Row A) (hne : ↑p ≠ []) : (twoRowSwap hA p hne) p = concatRow hA p hne

theorem FirstOrder.Language.FiberAssembly.twoRowSwap_apply_right {U : Type u} [LinearOrder U] {A : ℕ → Set U} (hA : Nested A) (p : Row A) (hne : ↑p ≠ []) : (twoRowSwap hA p hne) (concatRow hA p hne) = p

theorem FirstOrder.Language.FiberAssembly.twoRow_matched {U : Type u} [LinearOrder U] {Bstar : Type u} {B : U → Type u} {A : ℕ → Set U} (hA : Nested A) (p : Row A) (hne : ↑p ≠ []) : Matched (twoRowSwap hA p hne) ![Carrier.row p] ![Carrier.row (concatRow hA p hne)]

The row elements p and q are matched along the transposition.

theorem FirstOrder.Language.FiberAssembly.twoRow_bfEquiv {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} (hA : Nested A) (p : Row A) (hne : ↑p ≠ []) (β : Ordinal.{u_1}) (hβ : BFEquiv β 0 Fin.elim0 Fin.elim0) : BFEquiv β 1 ![Carrier.row p] ![Carrier.row (concatRow hA p hne)]

Two-row equivalence: if B u and B_* are equivalent at level β as structures, the row elements p and q are BFEquiv β in the assembled language.

theorem FirstOrder.Language.FiberAssembly.twoRow_not_automorphic {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] (hA : Nested A) (p : Row A) (hne : ↑p ≠ []) (hniso : IsEmpty (Lc.Equiv Bstar (B ((↑p).getLast hne)))) : ¬∃ (g : (lang U Lc).Equiv (PrefixCarrier Bstar B A) (PrefixCarrier Bstar B A)), g (Carrier.row p) = Carrier.row (concatRow hA p hne)

No automorphism carries p to q when B u ≇ B_*: restricting one to the differing fiber would give an isomorphism B_* ≃ B u. Relationality of Lc enters through restrictFiber.

theorem FirstOrder.Language.FiberAssembly.twoRow_lt_orbitRank {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 (PrefixCarrier Bstar B A)] (hA : Nested A) (p : Row A) (hne : ↑p ≠ []) (β : Ordinal.{u}) (hβ : BFEquiv β 0 Fin.elim0 Fin.elim0) (hniso : IsEmpty (Lc.Equiv Bstar (B ((↑p).getLast hne)))) : β < orbitRank ![Carrier.row p]

Orbit-rank corollary, the only statement using countability: in a countable assembled structure, the orbit rank of the row p exceeds β.