FiniteReindex

Part of the dependency closure of the small undecidable group constructions.

noncomputable def Undecidability.Thue.Matiyasevich1993.FiniteReindex.ruleCount {α : Type u_1} (T : ThueSystem α) (hT : Set.Finite T) : ℕ

Number of genuine relations in a finite set.

Equations

• Undecidability.Thue.Matiyasevich1993.FiniteReindex.ruleCount T hT = Fintype.card ↑T

noncomputable def Undecidability.Thue.Matiyasevich1993.FiniteReindex.ruleEquiv {α : Type u_1} (T : ThueSystem α) (hT : Set.Finite T) : ↑T ≃ Fin (ruleCount T hT)

An enumeration equivalence between a finite Thue relation set and a finite index type.

Equations

• Undecidability.Thue.Matiyasevich1993.FiniteReindex.ruleEquiv T hT = Fintype.equivFin ↑T

noncomputable def Undecidability.Thue.Matiyasevich1993.FiniteReindex.enumeratedF {α : Type u_1} (T : ThueSystem α) (hT : Set.Finite T) : Fin (ruleCount T hT + 1) → List α

Enumerate a finite relation set and adjoin one harmless identity rule at index zero. The extra rule makes the index type provably nonempty even when the supplied set happens to be empty.

Equations

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

noncomputable def Undecidability.Thue.Matiyasevich1993.FiniteReindex.enumeratedE {α : Type u_1} (T : ThueSystem α) (hT : Set.Finite T) : Fin (ruleCount T hT + 1) → List α

The right-hand rule words of a finite enumeration with an additional empty identity rule.

Equations

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

theorem Undecidability.Thue.Matiyasevich1993.FiniteReindex.enumeratedSystem_eq {α : Type u_1} (T : ThueSystem α) (hT : Set.Finite T) : finiteSystem (enumeratedF T hT) (enumeratedE T hT) = insert ([], []) T

theorem Undecidability.Thue.Matiyasevich1993.FiniteReindex.insert_identity_iff {α : Type u_1} (T : ThueSystem α) (X Y : List α) : ThueEq (insert ([], []) T) X Y ↔ ThueEq T X Y

theorem Undecidability.Thue.Matiyasevich1993.FiniteReindex.enumerated_iff {α : Type u_1} (T : ThueSystem α) (hT : Set.Finite T) (X Y : List α) : ThueEq (finiteSystem (enumeratedF T hT) (enumeratedE T hT)) X Y ↔ ThueEq T X Y

def Undecidability.Thue.Matiyasevich1993.FiniteReindex.mapWord {α : Type u_1} {β : Type u_2} (e : α ≃ β) (W : List α) : List β

Homomorphic word transport along an equivalence of finite alphabets.

Equations

• Undecidability.Thue.Matiyasevich1993.FiniteReindex.mapWord e W = List.map (⇑e) W

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.FiniteReindex.mapWord_append {α : Type u_1} {β : Type u_2} (e : α ≃ β) (X Y : List α) : mapWord e (X ++ Y) = mapWord e X ++ mapWord e Y

@[simp]

theorem Undecidability.Thue.Matiyasevich1993.FiniteReindex.mapWord_symm_mapWord {α : Type u_1} {β : Type u_2} (e : α ≃ β) (W : List α) : mapWord e.symm (mapWord e W) = W

theorem Undecidability.Thue.Matiyasevich1993.FiniteReindex.mapWord_computable {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] [Finite α] (e : α ≃ β) : Computable (mapWord e)

def Undecidability.Thue.Matiyasevich1993.FiniteReindex.mappedF {α : Type u_1} {β : Type u_2} {s : ℕ} (e : α ≃ β) (F : Fin s → List α) : Fin s → List β

The left-hand rule words transported along an alphabet equivalence.

Equations

• Undecidability.Thue.Matiyasevich1993.FiniteReindex.mappedF e F i = Undecidability.Thue.Matiyasevich1993.FiniteReindex.mapWord e (F i)

def Undecidability.Thue.Matiyasevich1993.FiniteReindex.mappedE {α : Type u_1} {β : Type u_2} {s : ℕ} (e : α ≃ β) (E : Fin s → List α) : Fin s → List β

The right-hand rule words transported along an alphabet equivalence.

Equations

• Undecidability.Thue.Matiyasevich1993.FiniteReindex.mappedE e E i = Undecidability.Thue.Matiyasevich1993.FiniteReindex.mapWord e (E i)

def Undecidability.Thue.Matiyasevich1993.FiniteReindex.alphabetEmbedding {α : Type u_1} {β : Type u_2} {s : ℕ} [Primcodable α] [Primcodable β] [Finite α] (e : α ≃ β) (F E : Fin s → List α) : Embedding (finiteSystem F E) (finiteSystem (mappedF e F) (mappedE e E))

The computable equivalence-reflecting Thue encoding induced by an alphabet equivalence.

Equations

• Undecidability.Thue.Matiyasevich1993.FiniteReindex.alphabetEmbedding e F E = { encode := Undecidability.Thue.Matiyasevich1993.FiniteReindex.mapWord e, encode_computable := ⋯, thueEq_iff := ⋯ }

theorem Undecidability.Thue.Matiyasevich1993.FiniteReindex.seed_of_finite_system {α : Type u_1} [Fintype α] [Nonempty α] [Primcodable α] (T : ThueSystem α) (hT : Set.Finite T) (P : List α) (hund : ¬ComputablePred fun (Q : List α) => ThueEq T Q P) : ∃ (seed : FiniteFixedTargetSeed), seed.alphabetSize = Fintype.card α ∧ seed.relationCount = ruleCount T hT + 1

Convert any finite fixed-target Thue problem over a nonempty finite alphabet into the exact Fin n/Fin r seed expected by the compression theorem.