Construction

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

def Undecidability.MillerTancer.oldGenerator {n : ℕ} (i : Fin n) : Fin (n + 3)

Include an old generator among the first n generators of the new presentation.

Equations

• Undecidability.MillerTancer.oldGenerator i = Fin.castAdd 3 i

def Undecidability.MillerTancer.oldWord {n : ℕ} (w : Word n) : Word (n + 3)

Include an old word in the enlarged alphabet.

Equations

• Undecidability.MillerTancer.oldWord w = Undecidability.Word.mapGenerators Undecidability.MillerTancer.oldGenerator w

def Undecidability.MillerTancer.alphaWord (n : ℕ) : Word (n + 3)

The three new words α, β, and γ.

Equations

• Undecidability.MillerTancer.alphaWord n = Undecidability.Word.generator (Fin.natAdd n 0)

def Undecidability.MillerTancer.betaWord (n : ℕ) : Word (n + 3)

The word representing the generator beta in this presentation.

Equations

• Undecidability.MillerTancer.betaWord n = Undecidability.Word.generator (Fin.natAdd n 1)

def Undecidability.MillerTancer.gammaWord (n : ℕ) : Word (n + 3)

The word representing the generator gamma in this presentation.

Equations

• Undecidability.MillerTancer.gammaWord n = Undecidability.Word.generator (Fin.natAdd n 2)

def Undecidability.MillerTancer.sigma₁ (n : ℕ) : Word (n + 3)

The relator σ₁ in the Miller--Tancer presentation.

Equations

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

def Undecidability.MillerTancer.sigma₂ (n : ℕ) : Word (n + 3)

The relator σ₂ in the Miller--Tancer presentation.

Equations

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

def Undecidability.MillerTancer.sigma₃ {n : ℕ} (w : Word n) : Word (n + 3)

The commutator relator σ₃(w) in the Miller--Tancer presentation; see the correction discussed in Remark 1.9 of the paper.

Equations

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

def Undecidability.MillerTancer.sigma₄ {n : ℕ} (z : Word n) : Word (n + 3)

The relator σ₄(z) in the Miller--Tancer presentation, using the single normal generator z.

Equations

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

def Undecidability.MillerTancer.additionalRelators {n : ℕ} (z w : Word n) : Fin 4 → Word (n + 3)

The four additional Miller--Tancer relators.

Equations

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

def Undecidability.MillerTancer.transform {n m : ℕ} (P : FP n m) (z w : Word n) : FP (n + 3) (m + 4)

The Miller--Tancer transformation: retain the m old relators and add three generators and four relators.

Equations

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

@[simp]

theorem Undecidability.MillerTancer.transform_old {n m : ℕ} (P : FP n m) (z w : Word n) (i : Fin m) : (transform P z w).relator (Fin.castAdd 4 i) = oldWord (P.relator i)

@[simp]

theorem Undecidability.MillerTancer.transform_additional {n m : ℕ} (P : FP n m) (z w : Word n) (i : Fin 4) : (transform P z w).relator (Fin.natAdd m i) = additionalRelators z w i

theorem Undecidability.MillerTancer.transform_computable {n m : ℕ} (P : FP n m) (z : Word n) : Computable₂ fun (w : Word n) (i : Fin (m + 4)) => (transform P z w).relator i

The word-indexed transformation is uniform and computable.

theorem Undecidability.MillerTancer.presentsTrivial_transform_of_wordProblem {n m : ℕ} (P : FP n m) (z : Word n) (hz : P.NormallyGenerates z) (w : Word n) (hw : P.wordProblem w) : (transform P z w).presentsTrivial

The elementary half of the Miller--Tancer argument.