Gordon's Lemma 2.1 and its specialization to the three-nine host.

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

Gordon's transformed presentation is trivial exactly when the input word is trivial in the host group.

def Undecidability.Gordon.family {n m : ℕ} (P : FP n m) (data : TorsionData P) : ℕ → FP 2 (m + 1)

The effective family obtained by enumerating the input words and transforming their presentations.

Equations

• Undecidability.Gordon.family P data j = Undecidability.Gordon.transform P data (Undecidability.wordOfNat n j)

theorem Undecidability.Gordon.family_isAdianRabin {n m : ℕ} (P : FP n m) (data : TorsionData P) (hP : ¬ComputablePred P.wordProblem) : FP.IsAdianRabinFamily (family P data)

theorem Undecidability.Gordon.lemma_2_1 {n m : ℕ} (P : FP n m) (condition : Condition21 P) (hP : ¬ComputablePred P.wordProblem) : ∃ (A : ℕ → FP 2 (m + 1)), FP.IsAdianRabinFamily A

Gordon's Lemma 2.1: condition (2.1) and an unsolvable host word problem give a two-generator Adian--Rabin family with one more relator.

def Undecidability.Host.gordonCondition21 (datum : Thue.StandingDatum) : Gordon.Condition21 (presentationOf datum)

Gordon's printed condition (2.1) for the host, using the generator D, whose abelianized image is trivial (and therefore has order one).

Equations

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