Documentation

InfinitaryLogic.ModelTheory.FiberOwnerRows

Adding owner rows to a tuple #

Every element of an assembled carrier has an owner row: a point pt r τ x is owned by row r, and a row is its own owner (owner, ownerRow).

Theorem (bfEquiv_append_ownerRows): if a ≡_{β + n} b for n-tuples, then appending the owner rows gives a ++ ownerRow a ≡_β b ++ ownerRow b. One block move (BFEquiv.forth_block) answers the whole owner tuple at once; the answer is then identified atomically at level 0: for a point coordinate the own atom forces the answer to be the owner of the matched point, and for a row coordinate the equality atom (a row is its own owner) together with the row atom forces it.

The cost β + n is sufficient, not claimed optimal. The statement covers empty tuples, repeated owners, and owners already present among the coordinates; the appended tuple is n rows long regardless.

source
def FirstOrder.Language.FiberAssembly.owner {U R : Type u} {C : R → Label U → Type u} :
Carrier R C → R

The owner row of an element: a point is owned by its row, a row by itself.

Equations
Instances For
    source
    @[simp]
    theorem FirstOrder.Language.FiberAssembly.owner_row {U R : Type u} {C : R → Label U → Type u} (r : R) :
    owner (Carrier.row r) = r
    source
    @[simp]
    theorem FirstOrder.Language.FiberAssembly.owner_pt {U R : Type u} {C : R → Label U → Type u} (r : R) (τ : Label U) (x : C r τ) :
    owner (Carrier.pt r τ x) = r
    source
    def FirstOrder.Language.FiberAssembly.ownerRow {U R : Type u} {C : R → Label U → Type u} {n : ℕ} (a : Fin n → Carrier R C) :
    Fin n → Carrier R C

    The owner rows of a tuple, coordinatewise.

    Equations
    Instances For
      source
      @[simp]
      theorem FirstOrder.Language.FiberAssembly.ownerRow_apply {U R : Type u} {C : R → Label U → Type u} {n : ℕ} (a : Fin n → Carrier R C) (i : Fin n) :
      ownerRow a i = Carrier.row (owner (a i))
      source
      theorem FirstOrder.Language.FiberAssembly.bfEquiv_append_ownerRows {U : Type u} {Lc : Language} {R : Type u} {C : R → Label U → Type u} {S : Type u} {D : S → Label U → Type u} [(r : R) → (τ : Label U) → Lc.Structure (C r τ)] [(s : S) → (τ : Label U) → Lc.Structure (D s τ)] {β : Ordinal.{u_1}} {n : ℕ} {a : Fin n → Carrier R C} {b : Fin n → Carrier S D} (h : BFEquiv (β + ↑n) n a b) :
      BFEquiv β (n + n) (Fin.append a (ownerRow a)) (Fin.append b (ownerRow b))

      Owner rows at finite cost. From a ≡_{β + n} b, appending the owner rows gives a ++ ownerRow a ≡_β b ++ ownerRow b.