The fixed machine-to-Thue seed and Matiyasevich's proved compression theorem together supply the exact three-relation binary input used by the host-group construction.

theorem Undecidability.Thue.has_undecidable_three_rule_system : Matiyasevich1993.HasUndecidableThreeRuleSystem

Matiyasevich's fixed-target binary three-relation system, derived from the fixed universal-machine seed.

def Undecidability.Thue.etaLetter (a : Fin 2) : List (Fin 2)

η(x) = s₁s₂²s₁ and η(y) = s₁s₂³s₁.

Equations

• Undecidability.Thue.etaLetter a = if a = 0 then [0, 1, 1, 0] else [0, 1, 1, 1, 0]

def Undecidability.Thue.eta (w : List (Fin 2)) : List (Fin 2)

The synchronizing monoid homomorphism, represented on lists.

Equations

• Undecidability.Thue.eta w = List.flatMap Undecidability.Thue.etaLetter w

def Undecidability.Thue.encodedF (U₃ : List (Fin 2)) : Fin 3 → List (Fin 2)

The left-hand words of the three rules after the standing binary encoding.

Equations

• Undecidability.Thue.encodedF U₃ i = Undecidability.Thue.eta (Undecidability.Thue.baseF U₃ i)

def Undecidability.Thue.encodedE (V₃ : List (Fin 2)) : Fin 3 → List (Fin 2)

The right-hand words of the three rules after the standing binary encoding.

Equations

• Undecidability.Thue.encodedE V₃ i = Undecidability.Thue.eta (Undecidability.Thue.baseE V₃ i)

def Undecidability.Thue.systemOf (F E : Fin 3 → List (Fin 2)) : ThueSystem (Fin 2)

The three-rule Thue system specified by indexed left-hand and right-hand words.

Equations

• Undecidability.Thue.systemOf F E = Set.range fun (i : Fin 3) => (F i, E i)

def Undecidability.Thue.encodedSystem (U₃ V₃ : List (Fin 2)) : ThueSystem (Fin 2)

The standing binary Thue system obtained by encoding the three base rules.

Equations

• Undecidability.Thue.encodedSystem U₃ V₃ = Undecidability.Thue.systemOf (Undecidability.Thue.encodedF U₃) (Undecidability.Thue.encodedE V₃)

def Undecidability.Thue.ContainsBoth (w : List (Fin 2)) : Prop

A two-letter positive word contains both alphabet symbols.

Equations

• Undecidability.Thue.ContainsBoth w = (0 ∈ w ∧ 1 ∈ w)

theorem Undecidability.Thue.containsBoth_ne_nil {w : List (Fin 2)} (h : ContainsBoth w) : w ≠ []

def Undecidability.Thue.evalPositive {G : Type u_1} [Group G] (s₁ s₂ : G) (w : List (Fin 2)) : G

Evaluate a positive two-letter word at two elements of a group.

Equations

• Undecidability.Thue.evalPositive s₁ s₂ w = (List.map (fun (i : Fin 2) => if i = 0 then s₁ else s₂) w).prod

structure Undecidability.Thue.BinaryRuleWords : Type

The three binary rule pairs and their fixed target word.

• F : Fin 3 → List (Fin 2)

  The three left sides of the rewriting rules.

• E : Fin 3 → List (Fin 2)

  The corresponding right sides.

• P : List (Fin 2)

  The fixed word whose reachability is tested.

structure Undecidability.Thue.StandingDatumextends Undecidability.Thue.BinaryRuleWords : Type

The exact Thue-system interface used by the remainder of the construction. The fields correspond to properties (a), (b), and (c) at the beginning of Section 2 of the paper.

• F : Fin 3 → List (Fin 2)
• E : Fin 3 → List (Fin 2)
• P : List (Fin 2)
• F_nonempty (i : Fin 3) : self.F i ≠ []
• E_nonempty (i : Fin 3) : self.E i ≠ []
• F_support (i : Fin 3) : ContainsBoth (self.F i)
• E_support (i : Fin 3) : ContainsBoth (self.E i)
• P_support : ContainsBoth self.P
• undecidable : ¬ComputablePred fun (Q : List (Fin 2)) => ThueEq (systemOf self.F self.E) Q self.P
• kill {G : Type} [Group G] (s₁ s₂ : G) : s₂ = s₁⁻¹ → evalPositive s₁ s₂ (self.F 1) = evalPositive s₁ s₂ (self.E 1) → s₁ = 1 ∧ s₂ = 1

theorem Undecidability.Thue.eta_computable : Computable eta

The synchronizing code is computable.

@[simp]

theorem Undecidability.Thue.eta_cons (a : Fin 2) (w : List (Fin 2)) : eta (a :: w) = etaLetter a ++ eta w

theorem Undecidability.Thue.baseF_nonempty (U₃ : List (Fin 2)) (hU₃ : U₃ ≠ []) (i : Fin 3) : baseF U₃ i ≠ []

theorem Undecidability.Thue.baseE_nonempty (V₃ : List (Fin 2)) (hV₃ : V₃ ≠ []) (i : Fin 3) : baseE V₃ i ≠ []

theorem Undecidability.Thue.synchronization (U₃ V₃ X Y : List (Fin 2)) (hU₃ : U₃ ≠ []) (hV₃ : V₃ ≠ []) : ThueEq (baseSystem U₃ V₃) X Y ↔ ThueEq (encodedSystem U₃ V₃) (eta X) (eta Y)

Every rewrite between encoded words uniquely decodes. The nonemptiness hypotheses exclude rules with an empty side, which could be applied away from a codeword boundary.

theorem Undecidability.Thue.eta_containsBoth {w : List (Fin 2)} (hw : w ≠ []) : ContainsBoth (eta w)

A nonempty encoded word contains both s₁ and s₂.

theorem Undecidability.Thue.encoded_second_rule_kills (U₃ V₃ : List (Fin 2)) {G : Type} [Group G] (s₁ s₂ : G) (hinv : s₂ = s₁⁻¹) (hrel : evalPositive s₁ s₂ (encodedF U₃ 1) = evalPositive s₁ s₂ (encodedE V₃ 1)) : s₁ = 1 ∧ s₂ = 1

The encoded second rule, together with s₂ = s₁⁻¹, kills both letters.

theorem Undecidability.Thue.encoded_undecidable {U₃ V₃ P₀ : List (Fin 2)} (hU₃ : U₃ ≠ []) (hV₃ : V₃ ≠ []) (h : ¬ComputablePred fun (Q : List (Fin 2)) => ThueEq (baseSystem U₃ V₃) Q P₀) : ¬ComputablePred fun (Q : List (Fin 2)) => ThueEq (encodedSystem U₃ V₃) Q (eta P₀)

Synchronization transfers fixed-target undecidability to the encoded system.

noncomputable def Undecidability.Thue.encodedDatum (U₃ V₃ P₀ : List (Fin 2)) (hU₃ : U₃ ≠ []) (hV₃ : V₃ ≠ []) (hP₀ : P₀ ≠ []) (hund : ¬ComputablePred fun (Q : List (Fin 2)) => ThueEq (baseSystem U₃ V₃) Q P₀) : StandingDatum

Package a nonempty Matiyasevich datum after synchronization.

Equations

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

theorem Undecidability.Thue.exists_standingDatum : Nonempty StandingDatum

There is a standing datum satisfying exactly (Und), (Supp), and (Kill).