The Hilbert-hotel row bijection of a companion

For an allowed path π and a threshold N, shiftRows hπ N : Row A ⊕ Unit ≃ Row A sends the path row to the prefix π|ₙ, each tail prefix π|ₖ with k ≥ N to π|ₖ₊₁, and every other row to itself. Its inverse sends π|ₙ back to the path row, π|ₖ₊₁ (k ≥ N) to π|ₖ, and fixes the rest. The case N = 0 shifts every prefix and sends the path row to the empty row.

This layer has no component language or structure parameters: it is a bijection of rows, well defined because prefixes of different lengths are different rows (prefixRow_injective). The tail-prefix predicate has the finite characterization isTailPrefix_iff: a row is a tail prefix iff its length is at least N and it is the prefix of its own length; no search over an unknown length is needed. The construction is noncomputable (classical decisions); no effectiveness is claimed.

Tail prefixes

def FirstOrder.Language.FiberAssembly.IsTailPrefix {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) (N : ℕ) (r : Row A) : Prop

A row is a tail prefix of π at threshold N: some π|ₖ with k ≥ N.

Equations

• FirstOrder.Language.FiberAssembly.IsTailPrefix hπ N r = ∃ (k : ℕ), N ≤ k ∧ r = FirstOrder.Language.FiberAssembly.prefixRow hπ k

theorem FirstOrder.Language.FiberAssembly.isTailPrefix_iff {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) (N : ℕ) (r : Row A) : IsTailPrefix hπ N r ↔ N ≤ (↑r).length ∧ r = prefixRow hπ (↑r).length

The finite characterization: a tail prefix is the prefix of its own length, which is at least N.

theorem FirstOrder.Language.FiberAssembly.isTailPrefix_prefixRow {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) {N k : ℕ} (hk : N ≤ k) : IsTailPrefix hπ N (prefixRow hπ k)

theorem FirstOrder.Language.FiberAssembly.not_isTailPrefix_of_length_lt {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) {N : ℕ} {r : Row A} (h : (↑r).length < N) : ¬IsTailPrefix hπ N r

theorem FirstOrder.Language.FiberAssembly.IsTailPrefix.length_ge {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} {hπ : IsAllowedPath A π} {N : ℕ} {r : Row A} (h : IsTailPrefix hπ N r) : N ≤ (↑r).length

The length of a tail prefix is at least N.

theorem FirstOrder.Language.FiberAssembly.IsTailPrefix.eq_prefixRow {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} {hπ : IsAllowedPath A π} {N : ℕ} {r : Row A} (h : IsTailPrefix hπ N r) : r = prefixRow hπ (↑r).length

A tail prefix is the prefix of its own length.

The bijection

noncomputable def FirstOrder.Language.FiberAssembly.shiftRows {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) (N : ℕ) : Row A ⊕ Unit ≃ Row A

The Hilbert-hotel row bijection at threshold N: the path row goes to π|ₙ, each tail prefix π|ₖ (k ≥ N) to π|ₖ₊₁, every other row to itself.

Equations

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

Forward equations

@[simp]

theorem FirstOrder.Language.FiberAssembly.shiftRows_inr {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) (N : ℕ) : (shiftRows hπ N) (Sum.inr ()) = prefixRow hπ N

theorem FirstOrder.Language.FiberAssembly.shiftRows_inl_prefixRow {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) {N k : ℕ} (hk : N ≤ k) : (shiftRows hπ N) (Sum.inl (prefixRow hπ k)) = prefixRow hπ (k + 1)

theorem FirstOrder.Language.FiberAssembly.shiftRows_inl_of_not {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) {N : ℕ} {r : Row A} (h : ¬IsTailPrefix hπ N r) : (shiftRows hπ N) (Sum.inl r) = r

Inverse equations

@[simp]

theorem FirstOrder.Language.FiberAssembly.shiftRows_symm_prefixRow {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) (N : ℕ) : (shiftRows hπ N).symm (prefixRow hπ N) = Sum.inr ()

theorem FirstOrder.Language.FiberAssembly.shiftRows_symm_prefixRow_succ {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) {N k : ℕ} (hk : N ≤ k) : (shiftRows hπ N).symm (prefixRow hπ (k + 1)) = Sum.inl (prefixRow hπ k)

theorem FirstOrder.Language.FiberAssembly.shiftRows_symm_of_not {U : Type u} [LinearOrder U] {A : ℕ → Set U} {π : ℕ → U} (hπ : IsAllowedPath A π) {N : ℕ} {r : Row A} (h : ¬IsTailPrefix hπ N r) : (shiftRows hπ N).symm r = Sum.inl r