Gordon's one-extra-relator construction

This file formalizes the presentation-theoretic part of Lemma 2.1 of Gordon (2022). The torsion hypothesis is recorded in the minimal form used in Gordon's proof: the selected abelianized generators have distinct orders, their orders have gcd one, and degree extends those orders injectively to all generators. (Gordon obtains this form by choosing a minimal witness to condition (2.1).)

structure Undecidability.Gordon.TorsionData {n m : ℕ} (P : FP n m) : Type

Proof-ready, minimal-witness form of condition (2.1) in Gordon's paper.

selected lists the generators used in (2.1), q gives their exact orders in the abelianization, and degree is the injective exponent assignment used in relations (iii)--(iv).

• p : ℕ

  The number of generators selected for the torsion condition.

• selected : Fin self.p ↪ Fin n

  The distinct generator indices selected for the torsion condition.

• q : Fin self.p → ℕ

  The prescribed orders of the selected generators in the abelianization.

• gcd_q : Finset.univ.gcd self.q = 1
• exactOrder (i : Fin self.p) : orderOf (Abelianization.of (PresentedGroup.of (self.selected i))) = self.q i
• degree : Fin n → ℕ

  The distinct positive exponents assigned to the original generators.

• degree_pos (i : Fin n) : 0 < self.degree i
• degree_injective : Function.Injective self.degree
• degree_selected (i : Fin self.p) : self.degree (self.selected i) = self.q i

def Undecidability.Gordon.aWord : Word 2

The word representing the generator a in this presentation.

Equations

• Undecidability.Gordon.aWord = Undecidability.Word.generator 0

def Undecidability.Gordon.bWord : Word 2

The word representing the generator b in this presentation.

Equations

• Undecidability.Gordon.bWord = Undecidability.Word.generator 1

def Undecidability.Gordon.alphaWord : Word 2

Eliminate alpha using a * alpha * a⁻¹ = b².

Equations

• Undecidability.Gordon.alphaWord = Undecidability.Word.product [Undecidability.Gordon.aWord.inverse, Undecidability.Gordon.bWord.pow 2, Undecidability.Gordon.aWord]

def Undecidability.Gordon.betaWord : Word 2

Eliminate beta using alpha * a * alpha⁻¹ = b * beta * b⁻¹.

Equations

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

def Undecidability.Gordon.rightConjugateWord (r : ℕ) : Word 2

Gordon's right-hand word beta⁻ʳ * b * betaʳ.

Equations

• Undecidability.Gordon.rightConjugateWord r = Undecidability.Word.product [(Undecidability.Gordon.betaWord.pow r).inverse, Undecidability.Gordon.bWord, Undecidability.Gordon.betaWord.pow r]

def Undecidability.Gordon.paperCommutator {n : ℕ} (u v : Word n) : Word n

The paper's commutator convention: [u,v] = u*v*u⁻¹*v⁻¹.

The project's older constructions use the opposite convention, so this is kept explicit.

Equations

• Undecidability.Gordon.paperCommutator u v = Undecidability.Word.product [u, v, u.inverse, v.inverse]

def Undecidability.Gordon.encodedGenerator {n m : ℕ} {P : FP n m} (data : TorsionData P) (i : Fin n) : Word 2

An old generator after eliminating alpha, beta, and the old generators from Gordon's presentation.

Equations

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

def Undecidability.Gordon.encodeWord {n m : ℕ} {P : FP n m} (data : TorsionData P) (w : Word n) : Word 2

Substitute the encoded two-generator words for a word in the old generators.

Equations

• Undecidability.Gordon.encodeWord data w = Undecidability.Word.substitute (Undecidability.Gordon.encodedGenerator data) w

@[simp]

theorem Undecidability.Gordon.eval_encodeWord {n m : ℕ} {P : FP n m} {H : Type u_1} [Group H] (data : TorsionData P) (x : Fin 2 → H) (w : Word n) : Word.eval x (encodeWord data w) = Word.eval (fun (i : Fin n) => Word.eval x (encodedGenerator data i)) w

def Undecidability.Gordon.additionalRelator {n m : ℕ} {P : FP n m} (data : TorsionData P) (w : Word n) : Word 2

The single relation left after all Tietze eliminations.

Equations

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

def Undecidability.Gordon.transform {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) : FP 2 (m + 1)

Gordon's two-generator, one-extra-relator presentation.

Equations

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

@[simp]

theorem Undecidability.Gordon.transform_old {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (i : Fin m) : (transform P data w).relator (Fin.castAdd 1 i) = encodeWord data (P.relator i)

@[simp]

theorem Undecidability.Gordon.transform_additional {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (i : Fin 1) : (transform P data w).relator (Fin.natAdd m i) = additionalRelator data w

theorem Undecidability.Gordon.encodeWord_primrec {n m : ℕ} (P : FP n m) (data : TorsionData P) : Primrec fun (w : Word n) => encodeWord data w

theorem Undecidability.Gordon.transform_computable {n m : ℕ} (P : FP n m) (data : TorsionData P) : Computable₂ fun (w : Word n) (i : Fin (m + 1)) => (transform P data w).relator i

The word-indexed Gordon transformation is uniform and computable.

theorem Undecidability.Gordon.presentsTrivial_transform_of_wordProblem {n m : ℕ} (P : FP n m) (data : TorsionData P) (w : Word n) (hw : P.wordProblem w) : (transform P data w).presentsTrivial

If the input word is trivial, Gordon's transformed presentation is trivial. This is the elementary half of Lemma 2.1.