This file isolates the reduction proved in Section 2 of Matiyasevich's "Word Problem for Thue Systems with a Few Relations" (1995) from the downstream construction of the standing Thue datum.

The paper starts with an arbitrary finite Thue system T₀, passes through systems T₁ and T₂, and finishes with the binary three-relation system

• ddcc ↔ cdd,
• ddcdc ↔ cdd,
• ρ₂(L) ↔ ρ₂(M).

With d = 0 and c = 1, and with the first two relations exchanged, this is definitionally the system Thue.baseSystem used by the project.

def Undecidability.Thue.Matiyasevich1993.finiteSystem {α : Type u_1} {r : ℕ} (F E : Fin r → List α) : ThueSystem α

A finite Thue system whose relations are explicitly indexed.

Equations

• Undecidability.Thue.Matiyasevich1993.finiteSystem F E = Set.range fun (i : Fin r) => (F i, E i)

structure Undecidability.Thue.Matiyasevich1993.Embedding {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (S : ThueSystem α) (T : ThueSystem β) : Type (max u_1 u_2)

A computable, equivalence-reflecting encoding of one Thue system into another. This is equivalence (10) in the paper.

• encode : List α → List β

  The computable word encoding of an equivalence-reflecting Thue-system embedding.

• encode_computable : Computable self.encode
• thueEq_iff (X Y : List α) : ThueEq S X Y ↔ ThueEq T (self.encode X) (self.encode Y)

def Undecidability.Thue.Matiyasevich1993.Embedding.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {S : ThueSystem α} {T : ThueSystem β} {U : ThueSystem γ} (g : Embedding T U) (f : Embedding S T) : Embedding S U

Equivalence-reflecting encodings compose.

Equations

• g.comp f = { encode := g.encode ∘ f.encode, encode_computable := ⋯, thueEq_iff := ⋯ }

theorem Undecidability.Thue.Matiyasevich1993.Embedding.target_undecidable {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {S : ThueSystem α} {T : ThueSystem β} (f : Embedding S T) (P : List α) (h : ¬ComputablePred fun (Q : List α) => ThueEq S Q P) : ¬ComputablePred fun (Q : List β) => ThueEq T Q (f.encode P)

Fixed-target undecidability is transported by an embedding.

structure Undecidability.Thue.Matiyasevich1993.FiniteFixedTargetSeed : Type

The exact finite seed needed from the machine-to-Thue bridge.

No nonemptiness condition on the sides of the seed relations is needed: Matiyasevich's first padding stage makes all sides nonempty. Positivity of the alphabet and relation index types avoids degenerate enumerations in the formulas of Sections 2.2--2.4. The machine construction naturally supplies both.

• alphabetSize : ℕ

  The number of letters in the finite seed alphabet.

• relationCount : ℕ

  The number of rules in the finite seed Thue system.

• alphabetSize_pos : 0 < self.alphabetSize
• relationCount_pos : 0 < self.relationCount
• F : Fin self.relationCount → List (Fin self.alphabetSize)

  The indexed left-hand words of the finite seed rules.

• E : Fin self.relationCount → List (Fin self.alphabetSize)

  The indexed right-hand words of the finite seed rules.

• P : List (Fin self.alphabetSize)

  The fixed target word whose Thue-equivalence class is undecidable.

• undecidable : ¬ComputablePred fun (Q : List (Fin self.alphabetSize)) => ThueEq (finiteSystem self.F self.E) Q self.P

def Undecidability.Thue.Matiyasevich1993.HasUndecidableThreeRuleSystem : Prop

Existence of a binary three-relation Thue system with an undecidable fixed-target word problem.

Equations

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

def Undecidability.Thue.Matiyasevich1993.CompressionTheorem : Prop

The precise mathematical content required from Section 2 of the 1995 paper. The encoding is nonempty even on the empty source word because the first two stages append their marker words.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.has_undecidable_three_rule_system_of_compression (hcompression : CompressionTheorem) (seed : FiniteFixedTargetSeed) : HasUndecidableThreeRuleSystem

The three-stage compression theorem sends any finite fixed-target seed to an undecidable binary three-relation system.