The row-selection combinatorics behind the displayed identity on page 49. selectOdd keeps positions 1,3,5,...; iterating it u times keeps the positions congruent to 2^u - 1 modulo 2^u.

def Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd {α : Type u_1} : List α → List α

Keep every second entry, starting with the second.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd (head :: y :: rest) = y :: Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd rest
• Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd x✝ = []

def Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin {α : Type u_1} : ℕ → List α → List α

Iterate selectOdd.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin 0 x✝ = x✝

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd_nil {α : Type u_1} : selectOdd [] = []

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd_cons_cons {α : Type u_1} (x y : α) (W : List α) : selectOdd (x :: y :: W) = y :: selectOdd W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin_succ {α : Type u_1} (u : ℕ) (W : List α) : thin (u + 1) W = selectOdd (thin u W)

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin_nil {α : Type u_1} (u : ℕ) : thin u [] = []

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd_length {α : Type u_1} (W : List α) : (selectOdd W).length = W.length / 2

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd_getD {α : Type u_1} (W : List α) (i : ℕ) (d : α) : (selectOdd W).getD i d = W.getD (2 * i + 1) d

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin_length {α : Type u_1} (u : ℕ) (W : List α) : (thin u W).length = W.length / 2 ^ u

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin_getD {α : Type u_1} (u : ℕ) (W : List α) (i : ℕ) (d : α) : (thin u W).getD i d = W.getD (2 ^ u * (i + 1) - 1) d

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd_append_of_even {α : Type u_1} (X Y : List α) (heven : 2 ∣ X.length) : selectOdd (X ++ Y) = selectOdd X ++ selectOdd Y

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin_append_of_dvd {α : Type u_1} (u : ℕ) (X Y : List α) (hdiv : 2 ^ u ∣ X.length) : thin u (X ++ Y) = thin u X ++ thin u Y

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin_succ_comm {α : Type u_1} (u : ℕ) (W : List α) : thin (u + 1) W = thin u (selectOdd W)

Aligned expansion

def Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.expand (u : ℕ) : List (Fin 2) → List (Fin 2)

Insert 2^u - 1 zeroes before every binary letter. The original letters then occupy precisely the positions congruent to 2^u - 1 modulo 2^u.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.expand u [] = []
• Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.expand u (x_1 :: W) = List.replicate (2 ^ u - 1) 0 ++ x_1 :: Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.expand u W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.expand_cons (u : ℕ) (x : Fin 2) (W : List (Fin 2)) : expand u (x :: W) = List.replicate (2 ^ u - 1) 0 ++ x :: expand u W

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.expand_length (u : ℕ) (W : List (Fin 2)) : (expand u W).length = W.length * 2 ^ u

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.expand_length_dvd (u : ℕ) (W : List (Fin 2)) : 2 ^ u ∣ (expand u W).length

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd_expandBlock (k : ℕ) (x : Fin 2) : selectOdd (List.replicate (2 * k + 1) 0 ++ [x]) = List.replicate k 0 ++ [x]

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin_expandBlock (u : ℕ) (x : Fin 2) : thin u (List.replicate (2 ^ u - 1) 0 ++ [x]) = [x]

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin_expand (u : ℕ) (W : List (Fin 2)) : thin u (expand u W) = W

thin is a left inverse to aligned expansion.

Reading a column-major transpose

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.column_getD {t : ℕ} (rows : Fin t → List (Fin 2)) (col : ℕ) (i : Fin t) : (column rows col).getD (↑i) 0 = (rows i).getD col 0

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.columnsFrom_getD {t : ℕ} (rows : Fin t → List (Fin 2)) (start width col : ℕ) (i : Fin t) (hcol : col < width) : (columnsFrom rows start width).getD (col * t + ↑i) 0 = (rows i).getD (start + col) 0

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.transpose_getD {t width : ℕ} (rows : Fin t → List (Fin 2)) (col : ℕ) (i : Fin t) (hcol : col < width) : (transpose width rows).getD (col * t + ↑i) 0 = (rows i).getD col 0

The padded row selected by e^u

def Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.paddedTransposeLast {t : ℕ} (width : ℕ) (rows : Fin t → List (Fin 2)) (j : Fin t) (z : Fin 2) : List (Fin 2)

Padded transpose whose last sampled padding symbol is an arbitrary bit z.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.paddedTransposeLast_length {t width : ℕ} (rows : Fin t → List (Fin 2)) (j : Fin t) (z : Fin 2) : (paddedTransposeLast width rows j z).length = (width + 1) * t

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.paddedTransposeLast_getD_row {t width : ℕ} (rows : Fin t → List (Fin 2)) (j : Fin t) (z : Fin 2) (ht : 0 < t) (col : ℕ) (hcol : col < width) : (paddedTransposeLast width rows j z).getD (t * (col + 1) - 1) 0 = (rows j).getD col 0

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.paddedTransposeLast_getD_last {t width : ℕ} (rows : Fin t → List (Fin 2)) (j : Fin t) (z : Fin 2) (ht : 0 < t) : (paddedTransposeLast width rows j z).getD (t * (width + 1) - 1) 0 = z

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin_paddedTranspose_last (u width : ℕ) (rows : Fin (2 ^ u) → List (Fin 2)) (j : Fin (2 ^ u)) (z : Fin 2) (hlen : ∀ (i : Fin (2 ^ u)), (rows i).length = width) : thin u (paddedTransposeLast width rows j z) = rows j ++ [z]

General row selection with an arbitrary final sampled bit.

Priority normalization performs the sampling

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.pushE_liftBinary_even (W : List (Fin 2)) (v : ℕ) (heven : 2 ∣ W.length) : pushE (liftBinary W ++ List.replicate v e) = liftBinary (selectOdd W) ++ List.replicate (v + 1) e

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.firstNormal_replicate_e_liftBinary (u : ℕ) (W : List (Fin 2)) (hdiv : 2 ^ u ∣ W.length) : firstNormal (List.replicate u e ++ liftBinary W) = liftBinary (thin u W) ++ List.replicate u e

An initial block e^u implements thin u on a binary word whose length is a multiple of 2^u.

The last column

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.columnsFrom_last {t : ℕ} (rows : Fin t → List (Fin 2)) (start k : ℕ) : columnsFrom rows start (k + 1) = columnsFrom rows start k ++ column rows (start + k)

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.column_last {t width : ℕ} (rows : Fin t → List (Fin 2)) (hwidth : 0 < width) (hlen : ∀ (i : Fin t), (rows i).length = width) (hend : ∀ (i : Fin t), ∃ (init : List (Fin 2)), rows i = init ++ [1]) : column rows (width - 1) = List.replicate t 1

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.transpose_ends_b {t width : ℕ} (rows : Fin t → List (Fin 2)) (ht : 0 < t) (hwidth : 0 < width) (hlen : ∀ (i : Fin t), (rows i).length = width) (hend : ∀ (i : Fin t), ∃ (init : List (Fin 2)), rows i = init ++ [1]) : ∃ (init : List (Fin 2)), transpose width rows = init ++ [1]

If every nonempty rectangular row ends in the binary letter 1, then the column-major transpose also ends in 1 (the final entry of its final column).

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.liftBinary_transpose_ends_b {t width : ℕ} (rows : Fin t → List (Fin 2)) (ht : 0 < t) (hwidth : 0 < width) (hlen : ∀ (i : Fin t), (rows i).length = width) (hend : ∀ (i : Fin t), ∃ (init : List (Fin 2)), rows i = init ++ [1]) : ∃ (init : List A₂), liftBinary (transpose width rows) = init ++ [b]

An affine variant of thin. Whereas thin u keeps the positions 2^u - 1, 2 * 2^u - 1, ..., affineSample u j keeps the positions j, j + 2^u, .... This makes the phase-neutrality of a transposed block of length width * 2^u explicit.

def Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.affineSample (u : ℕ) (j : Fin (2 ^ u)) (W : List (Fin 2)) : List (Fin 2)

Keep the entries whose zero-based indices are congruent to j modulo 2^u.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.affineSample u j W = Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.thin u (List.replicate (2 ^ u - 1 - ↑j) 0 ++ W)

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.affineSample_length (u : ℕ) (j : Fin (2 ^ u)) (W : List (Fin 2)) : (affineSample u j W).length = (2 ^ u - 1 - ↑j + W.length) / 2 ^ u

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.affineSample_getD (u : ℕ) (j : Fin (2 ^ u)) (W : List (Fin 2)) (k : ℕ) : (affineSample u j W).getD k 0 = W.getD (2 ^ u * k + ↑j) 0

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.affineSample_transpose_append (u width : ℕ) (rows : Fin (2 ^ u) → List (Fin 2)) (j : Fin (2 ^ u)) (R : List (Fin 2)) (hlen : ∀ (i : Fin (2 ^ u)), (rows i).length = width) : affineSample u j (transpose width rows ++ R) = rows j ++ affineSample u j R

A column-major transpose occupies a whole number of sampling periods. Sampling it at phase j, followed by an arbitrary suffix, returns row j followed by the suffix sampled at the unchanged phase.

def Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.highPhase (u : ℕ) (j : Fin (2 ^ u)) : Fin (2 ^ (u + 1))

The inclusion of a row index into the upper half of the next power-of-two block.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.highPhase u j = ⟨↑j + 2 ^ u, ⋯⟩

def Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.lowPhase (u : ℕ) (j : Fin (2 ^ u)) : Fin (2 ^ (u + 1))

The inclusion of a row index into the lower half of the next power-of-two block.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.lowPhase u j = ⟨↑j, ⋯⟩

theorem Undecidability.Thue.Matiyasevich1993.Priority.RowSelection.selectOdd_prefix_affineSample (u : ℕ) (P : List (Fin 2)) (j : Fin (2 ^ u)) : ∃ (P' : List (Fin 2)) (j' : Fin (2 ^ (u + 1))), ∀ (W : List (Fin 2)), selectOdd (P ++ affineSample u j W) = P' ++ affineSample (u + 1) j' W

Prefixing an affine sample and applying selectOdd updates only the finite prefix and lifts the sampling phase by one binary digit. For an even prefix length the new phase is j + 2^u; for an odd prefix length it is j.