The downstream composition of Sections 2.3--2.5. The row-selection module is imported below once its contextual normalization theorem is available; the code-language lemmas here are independent of that combinatorics.

def Undecidability.Thue.Matiyasevich1993.PowerPadding.includeIndex {r : ℕ} (i : Fin r) : Fin (Priority.powerCount r)

Every original relation index occurs among the indices padded up to the least power of two.

Equations

• Undecidability.Thue.Matiyasevich1993.PowerPadding.includeIndex i = Fin.castLE ⋯ i

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.PowerPadding.paddedIndex_include {r : ℕ} (hr : 0 < r) (i : Fin r) : Priority.paddedIndex hr (includeIndex i) = i

theorem Undecidability.Thue.Matiyasevich1993.PowerPadding.finiteSystem_paddedSide {r : ℕ} {A : Type u_1} (hr : 0 < r) (F E : Fin r → List A) : finiteSystem (Priority.paddedSide hr F) (Priority.paddedSide hr E) = finiteSystem F E

Repeating the first relation until the relation count is a power of two does not change the underlying set of Thue relations.

def Undecidability.Thue.Matiyasevich1993.Precompression.relationCount (n r : ℕ) : ℕ

Number of relations after the positive common-length padding stage.

Equations

• Undecidability.Thue.Matiyasevich1993.Precompression.relationCount n r = r + (n + 1)

def Undecidability.Thue.Matiyasevich1993.Precompression.leftRows {n r : ℕ} (F E : Fin r → List (Fin n)) : Fin (relationCount n r) → List (Fin 2)

Left binary rows obtained after Sections 2.2 and 2.3.

Equations

• Undecidability.Thue.Matiyasevich1993.Precompression.leftRows F E = Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeF (Undecidability.Thue.Matiyasevich1993.Padding.stage₁F F E)

def Undecidability.Thue.Matiyasevich1993.Precompression.rightRows {n r : ℕ} (F E : Fin r → List (Fin n)) : Fin (relationCount n r) → List (Fin 2)

Right binary rows obtained after Sections 2.2 and 2.3.

Equations

• Undecidability.Thue.Matiyasevich1993.Precompression.rightRows F E = Undecidability.Thue.Matiyasevich1993.Binary.stage₂PrimeE (Undecidability.Thue.Matiyasevich1993.Padding.stage₁E F E)

def Undecidability.Thue.Matiyasevich1993.Precompression.leftWidth {n r : ℕ} (F E : Fin r → List (Fin n)) : ℕ

Common length of the left binary rows.

Equations

• Undecidability.Thue.Matiyasevich1993.Precompression.leftWidth F E = Undecidability.Thue.Matiyasevich1993.Padding.p F E * (n + 5)

def Undecidability.Thue.Matiyasevich1993.Precompression.rightWidth {n r : ℕ} (F E : Fin r → List (Fin n)) : ℕ

Common length of the right binary rows.

Equations

• Undecidability.Thue.Matiyasevich1993.Precompression.rightWidth F E = Undecidability.Thue.Matiyasevich1993.Padding.q F E * (n + 5)

theorem Undecidability.Thue.Matiyasevich1993.Precompression.relationCount_pos (n r : ℕ) : 0 < relationCount n r

theorem Undecidability.Thue.Matiyasevich1993.Precompression.leftWidth_pos {n r : ℕ} (F E : Fin r → List (Fin n)) : 0 < leftWidth F E

theorem Undecidability.Thue.Matiyasevich1993.Precompression.rightWidth_pos {n r : ℕ} (F E : Fin r → List (Fin n)) : 0 < rightWidth F E

theorem Undecidability.Thue.Matiyasevich1993.Precompression.leftWidth_ge_two {n r : ℕ} (F E : Fin r → List (Fin n)) : 2 ≤ leftWidth F E

theorem Undecidability.Thue.Matiyasevich1993.Precompression.rightWidth_ge_two {n r : ℕ} (F E : Fin r → List (Fin n)) : 2 ≤ rightWidth F E

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Precompression.leftRows_length {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (relationCount n r)) : (leftRows F E i).length = leftWidth F E

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Precompression.rightRows_length {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (relationCount n r)) : (rightRows F E i).length = rightWidth F E

theorem Undecidability.Thue.Matiyasevich1993.Precompression.stage₁F_nonempty {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (relationCount n r)) : Padding.stage₁F F E i ≠ []

theorem Undecidability.Thue.Matiyasevich1993.Precompression.stage₁E_nonempty {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (relationCount n r)) : Padding.stage₁E F E i ≠ []

theorem Undecidability.Thue.Matiyasevich1993.Precompression.leftRows_starts_aa {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (relationCount n r)) : ∃ (tail : List (Fin 2)), leftRows F E i = 0 :: 0 :: tail

theorem Undecidability.Thue.Matiyasevich1993.Precompression.rightRows_starts_aa {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (relationCount n r)) : ∃ (tail : List (Fin 2)), rightRows F E i = 0 :: 0 :: tail

theorem Undecidability.Thue.Matiyasevich1993.Precompression.rho₁_ends_b {N : ℕ} (W : List (Fin N)) (hW : W ≠ []) : ∃ (init : List (Fin 2)), Binary.rho₁ N W = init ++ [1]

Every nonempty word has a binary code ending in b.

theorem Undecidability.Thue.Matiyasevich1993.Precompression.leftRows_ends_b {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (relationCount n r)) : ∃ (init : List (Fin 2)), leftRows F E i = init ++ [1]

theorem Undecidability.Thue.Matiyasevich1993.Precompression.rightRows_ends_b {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (relationCount n r)) : ∃ (init : List (Fin 2)), rightRows F E i = init ++ [1]

def Undecidability.Thue.Matiyasevich1993.Precompression.embedding {n r : ℕ} (F E : Fin r → List (Fin n)) : Embedding (finiteSystem F E) (finiteSystem (leftRows F E) (rightRows F E))

The already verified first two stages, packaged as one embedding.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.Compression.noAAA_iff_not_infix {W : List Priority.A₂} : Priority.NoAAA W ↔ ¬[Priority.a, Priority.a, Priority.a] <:+: W

theorem Undecidability.Thue.Matiyasevich1993.Compression.noAAA_liftBinary {W : List (Fin 2)} (h : ¬∃ (l : List (Fin 2)) (r : List (Fin 2)), W = l ++ [0, 0, 0] ++ r) : Priority.NoAAA (Priority.liftBinary W)

Avoidance of 000 is preserved by the inclusion of the binary alphabet into {a,b,e}.

theorem Undecidability.Thue.Matiyasevich1993.Compression.noAAA_append_marker {W : List Priority.A₂} (hno : Priority.NoAAA W) (hend : W = [] ∨ ∃ (init : List Priority.A₂), W = init ++ [Priority.b]) (u : ℕ) : Priority.NoAAA (W ++ [Priority.a] ++ List.replicate u Priority.e)

Appending the marker a e^u preserves aaa-avoidance when the binary prefix is empty or ends in b.

theorem Undecidability.Thue.Matiyasevich1993.Compression.noAAA_encode_rho₁ {N u : ℕ} (W : List (Fin N)) : Priority.NoAAA (Priority.encode u (Binary.rho₁ N W))

The first-priority normal form of an encoded rho₁ word has no occurrence of aaa, including across its trailing marker.

The concrete long words

def Undecidability.Thue.Matiyasevich1993.Compression.u (n r : ℕ) : ℕ

The exponent and power-of-two row count used in Sections 2.3--2.4.

Equations

• Undecidability.Thue.Matiyasevich1993.Compression.u n r = Undecidability.Thue.Matiyasevich1993.Priority.exponent (Undecidability.Thue.Matiyasevich1993.Precompression.relationCount n r)

def Undecidability.Thue.Matiyasevich1993.Compression.t (n r : ℕ) : ℕ

The least power-of-two row count large enough for the precompressed relation set.

Equations

• Undecidability.Thue.Matiyasevich1993.Compression.t n r = Undecidability.Thue.Matiyasevich1993.Priority.powerCount (Undecidability.Thue.Matiyasevich1993.Precompression.relationCount n r)

theorem Undecidability.Thue.Matiyasevich1993.Compression.t_pos (n r : ℕ) : 0 < t n r

def Undecidability.Thue.Matiyasevich1993.Compression.paddedLeftRows {n r : ℕ} (F E : Fin r → List (Fin n)) : Fin (t n r) → List (Fin 2)

The binary rule rows, repeated to the least power of two.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Compression.paddedRightRows {n r : ℕ} (F E : Fin r → List (Fin n)) : Fin (t n r) → List (Fin 2)

The precompressed right-hand rule words padded to the power-of-two row count.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Compression.binarySystem {n r : ℕ} (F E : Fin r → List (Fin n)) : ThueSystem (Fin 2)

The binary Thue system formed by the padded precompressed rule rows.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.Compression.binarySystem_eq_unpadded {n r : ℕ} (F E : Fin r → List (Fin n)) : binarySystem F E = finiteSystem (Precompression.leftRows F E) (Precompression.rightRows F E)

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Compression.paddedLeftRows_length {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (t n r)) : (paddedLeftRows F E i).length = Precompression.leftWidth F E

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Compression.paddedRightRows_length {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (t n r)) : (paddedRightRows F E i).length = Precompression.rightWidth F E

theorem Undecidability.Thue.Matiyasevich1993.Compression.paddedLeftRows_starts_aa {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (t n r)) : ∃ (tail : List (Fin 2)), paddedLeftRows F E i = 0 :: 0 :: tail

theorem Undecidability.Thue.Matiyasevich1993.Compression.paddedRightRows_starts_aa {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (t n r)) : ∃ (tail : List (Fin 2)), paddedRightRows F E i = 0 :: 0 :: tail

theorem Undecidability.Thue.Matiyasevich1993.Compression.paddedLeftRows_ends_b {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (t n r)) : ∃ (init : List (Fin 2)), paddedLeftRows F E i = init ++ [1]

theorem Undecidability.Thue.Matiyasevich1993.Compression.paddedRightRows_ends_b {n r : ℕ} (F E : Fin r → List (Fin n)) (i : Fin (t n r)) : ∃ (init : List (Fin 2)), paddedRightRows F E i = init ++ [1]

theorem Undecidability.Thue.Matiyasevich1993.Compression.decode_binary_reachable {n r : ℕ} (F E : Fin r → List (Fin n)) (X : List (Fin n)) {W : List (Fin 2)} (h : ThueEq (binarySystem F E) ((Precompression.embedding F E).encode X) W) : ∃ (Z : List (Fin (n + 1))), W = Binary.rho₁ (n + 1) Z ∧ ThueEq (Padding.stage₁System F E) (Padding.encode F E X) Z

Any binary word reachable from the preceding encoding is still a rho₁-codeword. This is the synchronization fact from Section 2.3, transported across the harmless power-of-two relation padding.

theorem Undecidability.Thue.Matiyasevich1993.Compression.noAAA_of_binary_reachable {n r : ℕ} (F E : Fin r → List (Fin n)) (X : List (Fin n)) {W : List (Fin 2)} (h : ThueEq (binarySystem F E) ((Precompression.embedding F E).encode X) W) : Priority.NoAAA (Priority.encode (u n r) W)

def Undecidability.Thue.Matiyasevich1993.Compression.leftLong {n r : ℕ} (F E : Fin r → List (Fin n)) : List Priority.A₂

The long sides (24), converted to the alphabet {a,b,e}.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Compression.rightLong {n r : ℕ} (F E : Fin r → List (Fin n)) : List Priority.A₂

The transposed right-hand rule word lifted to the three-letter priority alphabet.

Equations

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

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Compression.leftLong_eCount {n r : ℕ} (F E : Fin r → List (Fin n)) : Priority.eCount (leftLong F E) = 0

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.Compression.rightLong_eCount {n r : ℕ} (F E : Fin r → List (Fin n)) : Priority.eCount (rightLong F E) = 0

theorem Undecidability.Thue.Matiyasevich1993.Compression.leftLong_length {n r : ℕ} (F E : Fin r → List (Fin n)) : (leftLong F E).length = Precompression.leftWidth F E * t n r

theorem Undecidability.Thue.Matiyasevich1993.Compression.rightLong_length {n r : ℕ} (F E : Fin r → List (Fin n)) : (rightLong F E).length = Precompression.rightWidth F E * t n r

theorem Undecidability.Thue.Matiyasevich1993.Compression.leftLong_ne_nil {n r : ℕ} (F E : Fin r → List (Fin n)) : leftLong F E ≠ []

theorem Undecidability.Thue.Matiyasevich1993.Compression.rightLong_ne_nil {n r : ℕ} (F E : Fin r → List (Fin n)) : rightLong F E ≠ []

def Undecidability.Thue.Matiyasevich1993.Compression.U₃ {n r : ℕ} (F E : Fin r → List (Fin n)) : List (Fin 2)

The actual long words in the final two-letter, three-relation system.

Equations

• Undecidability.Thue.Matiyasevich1993.Compression.U₃ F E = Undecidability.Thue.Matiyasevich1993.rho₂ (Undecidability.Thue.Matiyasevich1993.Compression.leftLong F E)

def Undecidability.Thue.Matiyasevich1993.Compression.V₃ {n r : ℕ} (F E : Fin r → List (Fin n)) : List (Fin 2)

The final binary encoding of the transposed right-hand rule word.

Equations

• Undecidability.Thue.Matiyasevich1993.Compression.V₃ F E = Undecidability.Thue.Matiyasevich1993.rho₂ (Undecidability.Thue.Matiyasevich1993.Compression.rightLong F E)

theorem Undecidability.Thue.Matiyasevich1993.Compression.U₃_ne_nil {n r : ℕ} (F E : Fin r → List (Fin n)) : U₃ F E ≠ []

theorem Undecidability.Thue.Matiyasevich1993.Compression.V₃_ne_nil {n r : ℕ} (F E : Fin r → List (Fin n)) : V₃ F E ≠ []

def Undecidability.Thue.Matiyasevich1993.Compression.priorityEncode {n r : ℕ} (F E : Fin r → List (Fin n)) (W : List (Fin n)) : List Priority.A₂

The word map through the first priority system, before applying rho₂.

Equations

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

def Undecidability.Thue.Matiyasevich1993.Compression.fullEncode {n r : ℕ} (F E : Fin r → List (Fin n)) (W : List (Fin n)) : List (Fin 2)

The composed word map from T₀ to T₃.

Equations

• Undecidability.Thue.Matiyasevich1993.Compression.fullEncode F E W = Undecidability.Thue.Matiyasevich1993.rho₂ (Undecidability.Thue.Matiyasevich1993.Compression.priorityEncode F E W)

theorem Undecidability.Thue.Matiyasevich1993.Compression.fullEncode_computable {n r : ℕ} (F E : Fin r → List (Fin n)) : Computable (fullEncode F E)

theorem Undecidability.Thue.Matiyasevich1993.Compression.fullEncode_ne_nil {n r : ℕ} (F E : Fin r → List (Fin n)) (W : List (Fin n)) : fullEncode F E W ≠ []

Interface of the priority-stage proof

structure Undecidability.Thue.Matiyasevich1993.Compression.PriorityBridge {n r : ℕ} (F E : Fin r → List (Fin n)) : Prop

The shape, equivalence, and reachability invariants from Section 2.4 for words from the preceding encodings. The equivalence applies to encoded source words, rather than to arbitrary words of the intermediate system.

• leftShape : Priority.LongShape (2 * t n r) (leftLong F E)
• rightShape : Priority.LongShape (2 * t n r) (rightLong F E)
• thueEq_iff (X Y : List (Fin n)) : ThueEq (finiteSystem F E) X Y ↔ ThueEq (stage₂System (leftLong F E) (rightLong F E)) (priorityEncode F E X) (priorityEncode F E Y)
• reachableNoAAA (X : List (Fin n)) : Priority.ReachableNoAAA (leftLong F E) (rightLong F E) (priorityEncode F E X)

def Undecidability.Thue.Matiyasevich1993.Compression.embeddingOfBridge {n r : ℕ} (F E : Fin r → List (Fin n)) (bridge : PriorityBridge F E) : Embedding (finiteSystem F E) (baseSystem (U₃ F E) (V₃ F E))

The final decoder combines with PriorityBridge to give an equivalence-reflecting encoding into the three-relation system.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.Compression.compressionTheorem_of_priorityBridges (bridges : ∀ (n r : ℕ), 0 < n → 0 < r → ∀ (F E : Fin r → List (Fin n)), PriorityBridge F E) : CompressionTheorem

A bridge for every finite source system is the final ingredient of the public compression theorem.