The contextual form of the row-selection argument on page 50. The first priority block only tests whether a letter is e; consequently, once its normal form is clean (a binary word followed by all the e's), an arbitrary left context acts on the binary suffix by consing binary letters and applying selectOdd once for every e.

def Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.lowerBit (x : A₂) : Fin 2

Decode a non-e letter of A₂ to the binary alphabet.

Equations

• Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.lowerBit x = if x = Undecidability.Thue.Matiyasevich1993.Priority.a then 0 else 1

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.liftBit_lowerBit {x : A₂} (hx : x ≠ e) : liftBit (lowerBit x) = x

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.lowerBit_liftBit (x : Fin 2) : lowerBit (liftBit x) = x

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.pushE_clean_inv (W : List A₂) (B : List (Fin 2)) (v : ℕ) (hcount : eCount W = v) (hclean : pushE W = liftBinary B ++ List.replicate (v + 1) e) : ∃ (C : List (Fin 2)), W = liftBinary C ++ List.replicate v e ∧ 2 ∣ C.length ∧ RowSelection.selectOdd C = B

A clean output of pushE can only arise by sampling an even binary prefix followed by the existing block of e's.

The binary process represented by a clean normalization

def Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.process : List A₂ → List (Fin 2) → List (Fin 2)

Fold a left context over a binary suffix: binary letters are retained, while every e keeps every second letter of the state to its right.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.process [] x✝ = x✝

def Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.Processable : List A₂ → List (Fin 2) → Prop

Every e sees an even binary state. This is exactly the condition under which normalization finishes with all e's in one trailing block.

Equations

• One or more equations did not get rendered due to their size.
• Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.Processable [] x✝ = True

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.process_cons_e (l : List A₂) (W : List (Fin 2)) : process (e :: l) W = RowSelection.selectOdd (process l W)

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.process_cons_ne (x : A₂) (l : List A₂) (W : List (Fin 2)) (hx : x ≠ e) : process (x :: l) W = lowerBit x :: process l W

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.processable_cons_e_iff (l : List A₂) (W : List (Fin 2)) : Processable (e :: l) W ↔ Processable l W ∧ 2 ∣ (process l W).length

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.processable_cons_ne_iff (x : A₂) (l : List A₂) (W : List (Fin 2)) (hx : x ≠ e) : Processable (x :: l) W ↔ Processable l W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.eCount_e_cons (l : List A₂) : eCount (e :: l) = eCount l + 1

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.eCount_cons_ne (x : A₂) (l : List A₂) (hx : x ≠ e) : eCount (x :: l) = eCount l

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.firstNormal_eq_process (l : List A₂) (W : List (Fin 2)) (hvalid : Processable l W) : firstNormal (l ++ liftBinary W) = liftBinary (process l W) ++ List.replicate (eCount l) e

A processable context has the advertised clean first-priority normal form.

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.processable_of_firstNormal_clean (l : List A₂) (W B : List (Fin 2)) (hclean : firstNormal (l ++ liftBinary W) = liftBinary B ++ List.replicate (eCount l) e) : Processable l W ∧ process l W = B

Conversely, a clean normal form uniquely determines the binary process and proves all of its parity obligations.

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.process_periodic_shift (l : List A₂) (W₁ W₂ : List (Fin 2)) (k : ℕ) (hlen : W₂.length = W₁.length + k * 2 ^ eCount l) : (Processable l W₁ ↔ Processable l W₂) ∧ (process l W₂).length = (process l W₁).length + k

Changing the binary suffix length by a multiple of the full sampling period preserves every intermediate parity obligation. After all samplings, the output length changes by precisely the quotient k.

Affine description and phase-neutral transpose replacement

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.process_affine (l : List A₂) : ∃ (P : List (Fin 2)) (j : Fin (2 ^ eCount l)), ∀ (W : List (Fin 2)), process l W = P ++ RowSelection.affineSample (eCount l) j W

An arbitrary context acts affinely on every binary suffix: a fixed binary prefix is followed by one fixed residue class modulo 2^(eCount l).

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.process_replace_transpose (l : List A₂) (p q : ℕ) (leftRows rightRows : Fin (2 ^ eCount l) → List (Fin 2)) (R : List (Fin 2)) (hp : ∀ (i : Fin (2 ^ eCount l)), (leftRows i).length = p) (hq : ∀ (i : Fin (2 ^ eCount l)), (rightRows i).length = q) : ∃ (P : List (Fin 2)) (j : Fin (2 ^ eCount l)) (S : List (Fin 2)), process l (transpose p leftRows ++ R) = P ++ leftRows j ++ S ∧ process l (transpose q rightRows ++ R) = P ++ rightRows j ++ S

Replacing a rectangular transpose by another rectangular transpose keeps the fixed affine contexts and selects the same row index.

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.processable_replace_transpose (l : List A₂) (p q : ℕ) (leftRows rightRows : Fin (2 ^ eCount l) → List (Fin 2)) (R : List (Fin 2)) : Processable l (transpose p leftRows ++ R) ↔ Processable l (transpose q rightRows ++ R)

Since both transpose lengths are multiples of the full sampling period, replacing one by the other preserves clean processability.

The contextual same-row theorem

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.exists_liftBinary_of_eCount_zero {W : List A₂} (hW : eCount W = 0) : ∃ (B : List (Fin 2)), W = liftBinary B

A word with no e is uniquely in the image of the binary inclusion.

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.split_before_terminal_zero {P L S B : List (Fin 2)} (hend : ∃ (init : List (Fin 2)), L = init ++ [1]) (hword : P ++ L ++ S = B ++ [0]) : ∃ (S₀ : List (Fin 2)), S = S₀ ++ [0] ∧ B = P ++ L ++ S₀

If a block ending in 1 occurs immediately before a suffix and the whole word ends in the marker 0, then that marker belongs to the suffix.

theorem Undecidability.Thue.Matiyasevich1993.Priority.ContextualSelection.replace_transpose_clean (u p q : ℕ) (leftRows rightRows : Fin (2 ^ u) → List (Fin 2)) (hp : ∀ (i : Fin (2 ^ u)), (leftRows i).length = p) (hq : ∀ (i : Fin (2 ^ u)), (rightRows i).length = q) (hleftEnd : ∀ (i : Fin (2 ^ u)), ∃ (init : List (Fin 2)), leftRows i = init ++ [1]) {l r : List A₂} {B : List (Fin 2)} (hl : eCount l = u) (hr : eCount r = 0) (hclean : firstNormal (l ++ liftBinary (transpose p leftRows) ++ r) = encode u B) : ∃ (j : Fin (2 ^ u)) (left : List (Fin 2)) (right : List (Fin 2)), B = left ++ leftRows j ++ right ∧ firstNormal (l ++ liftBinary (transpose q rightRows) ++ r) = encode u (left ++ rightRows j ++ right)

Contextual row selection for a long-rule step. If the normal form of the left transpose is a clean encoded word, replacing it by any other rectangular transpose selects the same row index and leaves both binary contexts fixed.

The terminal-1 hypothesis distinguishes the last letter of a selected left row from the terminal a (binary 0) marker in encode.