Presentation

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

@[reducible, inline]

abbrev Undecidability.Host.HostWord : Type

Words on the compressed host generators d, s, z.

Equations

• Undecidability.Host.HostWord = Undecidability.Word 3

inductive Undecidability.Host.OldGen : Type

Names of the nine generators just before Tietze compression.

• d : OldGen
• e : OldGen
• s1 : OldGen
• s2 : OldGen
• c : OldGen
• t : OldGen
• k : OldGen
• y : OldGen
• z : OldGen

@[reducible, inline]

abbrev Undecidability.Host.OldWord : Type

Words on the nine-generator alphabet before the ordered Tietze eliminations.

Equations

• Undecidability.Host.OldWord = List (Undecidability.Host.OldGen × Bool)

def Undecidability.Host.OldWord.generator (g : OldGen) : OldWord

The positive one-letter word for an original generator.

Equations

• Undecidability.Host.OldWord.generator g = [(g, true)]

def Undecidability.Host.OldWord.inverse (w : OldWord) : OldWord

Reverse a word and invert each of its letters.

Equations

• w.inverse = FreeGroup.invRev w

def Undecidability.Host.OldWord.mul (u v : OldWord) : OldWord

Concatenate two words on the original generator alphabet.

Equations

• u.mul v = u ++ v

def Undecidability.Host.OldWord.product (ws : List OldWord) : OldWord

Concatenate the supplied list of original-alphabet words.

Equations

• Undecidability.Host.OldWord.product ws = ws.flatten

def Undecidability.Host.OldWord.pow (w : OldWord) (n : ℕ) : OldWord

Concatenate the indicated number of copies of an original-alphabet word.

Equations

• w.pow n = (List.replicate n w).flatten

def Undecidability.Host.OldWord.evaluate (sigma : OldGen → HostWord) (w : OldWord) : HostWord

Substitute a host word for each old generator, respecting signs.

Equations

• Undecidability.Host.OldWord.evaluate sigma w = Undecidability.Word.substitute sigma w

def Undecidability.Host.OldWord.positive (w : List (Fin 2)) : OldWord

Read a positive {s₁,s₂}-word in the old alphabet.

Equations

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

def Undecidability.Host.OldWord.relation (lhs rhs : OldWord) : OldWord

The relator word obtained from an equality of two original-alphabet words.

Equations

• lhs.relation rhs = lhs.mul rhs.inverse

def Undecidability.Host.OldWord.commutator (u v : OldWord) : OldWord

The paper's convention [u,v] = u⁻¹v⁻¹uv.

Equations

• u.commutator v = Undecidability.Host.OldWord.product [u.inverse, v.inverse, u, v]

@[simp]

theorem Undecidability.Host.OldWord.evaluate_generator (sigma : OldGen → HostWord) (g : OldGen) : evaluate sigma (generator g) = sigma g

@[simp]

theorem Undecidability.Host.OldWord.evaluate_mul (sigma : OldGen → HostWord) (u v : OldWord) : evaluate sigma (u.mul v) = Word.mul (evaluate sigma u) (evaluate sigma v)

@[simp]

theorem Undecidability.Host.OldWord.evaluate_inverse (sigma : OldGen → HostWord) (w : OldWord) : evaluate sigma w.inverse = Word.inverse (evaluate sigma w)

@[simp]

theorem Undecidability.Host.OldWord.evaluate_product (sigma : OldGen → HostWord) (ws : List OldWord) : evaluate sigma (product ws) = Word.product (List.map (evaluate sigma) ws)

@[simp]

theorem Undecidability.Host.OldWord.evaluate_pow (sigma : OldGen → HostWord) (w : OldWord) (n : ℕ) : evaluate sigma (w.pow n) = Word.pow (evaluate sigma w) n

@[simp]

theorem Undecidability.Host.OldWord.evaluate_relation (sigma : OldGen → HostWord) (lhs rhs : OldWord) : evaluate sigma (lhs.relation rhs) = Word.relation (evaluate sigma lhs) (evaluate sigma rhs)

@[simp]

theorem Undecidability.Host.OldWord.evaluate_commutator (sigma : OldGen → HostWord) (u v : OldWord) : evaluate sigma (u.commutator v) = Word.commutator (evaluate sigma u) (evaluate sigma v)

@[simp]

theorem Undecidability.Host.OldWord.evaluate_positive (sigma : OldGen → HostWord) (w : List (Fin 2)) : evaluate sigma (positive w) = Word.substitutePositive (sigma OldGen.s1) (sigma OldGen.s2) w

@[reducible, inline]

abbrev Undecidability.Host.od : OldWord

The one-letter original-alphabet word d.

Equations

• Undecidability.Host.od = Undecidability.Host.OldWord.generator Undecidability.Host.OldGen.d

@[reducible, inline]

abbrev Undecidability.Host.oe : OldWord

The one-letter original-alphabet word e.

Equations

• Undecidability.Host.oe = Undecidability.Host.OldWord.generator Undecidability.Host.OldGen.e

@[reducible, inline]

abbrev Undecidability.Host.os1 : OldWord

The one-letter original-alphabet word s₁.

Equations

• Undecidability.Host.os1 = Undecidability.Host.OldWord.generator Undecidability.Host.OldGen.s1

@[reducible, inline]

abbrev Undecidability.Host.oc : OldWord

The one-letter original-alphabet word c.

Equations

• Undecidability.Host.oc = Undecidability.Host.OldWord.generator Undecidability.Host.OldGen.c

@[reducible, inline]

abbrev Undecidability.Host.ot : OldWord

The one-letter original-alphabet word t.

Equations

• Undecidability.Host.ot = Undecidability.Host.OldWord.generator Undecidability.Host.OldGen.t

@[reducible, inline]

abbrev Undecidability.Host.ok : OldWord

The one-letter original-alphabet word k.

Equations

• Undecidability.Host.ok = Undecidability.Host.OldWord.generator Undecidability.Host.OldGen.k

@[reducible, inline]

abbrev Undecidability.Host.oy : OldWord

The one-letter original-alphabet word y.

Equations

• Undecidability.Host.oy = Undecidability.Host.OldWord.generator Undecidability.Host.OldGen.y

def Undecidability.Host.oldSimulationRelator (F E : Fin 3 → List (Fin 2)) (i : Fin 3) : OldWord

The ith Borisov simulation relation retained during the compression of Proposition 2.3 of the paper.

Equations

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

def Undecidability.Host.oldSurvivingRelator (F E : Fin 3 → List (Fin 2)) (P : List (Fin 2)) : Fin 9 → OldWord

The nine surviving relators, before applying the ordered substitution tau.

Equations

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

def Undecidability.Host.dWord : HostWord

Retained generators in order: D, S, Z.

Equations

• Undecidability.Host.dWord = Undecidability.Word.generator 0

def Undecidability.Host.sWord : HostWord

The retained host generator s.

Equations

• Undecidability.Host.sWord = Undecidability.Word.generator 1

def Undecidability.Host.zWord : HostWord

The retained host generator z.

Equations

• Undecidability.Host.zWord = Undecidability.Word.generator 2

def Undecidability.Host.tWord : HostWord

The substitution word z⁻¹ * d * z for t.

Equations

• Undecidability.Host.tWord = Undecidability.Word.product [Undecidability.Word.inverse Undecidability.Host.zWord, Undecidability.Host.dWord, Undecidability.Host.zWord]

def Undecidability.Host.cWord : HostWord

The substitution word z⁻¹ * t * z for c.

Equations

• Undecidability.Host.cWord = Undecidability.Word.product [Undecidability.Word.inverse Undecidability.Host.zWord, Undecidability.Host.tWord, Undecidability.Host.zWord]

def Undecidability.Host.yWord : HostWord

The substitution word z⁻¹ * c * z for y.

Equations

• Undecidability.Host.yWord = Undecidability.Word.product [Undecidability.Word.inverse Undecidability.Host.zWord, Undecidability.Host.cWord, Undecidability.Host.zWord]

def Undecidability.Host.eWord : HostWord

The substitution word y⁻¹ * d⁻¹ * y for e.

Equations

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

def Undecidability.Host.kWord : HostWord

The substitution word y⁻¹ * t * y for k.

Equations

• Undecidability.Host.kWord = Undecidability.Word.product [Undecidability.Word.inverse Undecidability.Host.yWord, Undecidability.Host.tWord, Undecidability.Host.yWord]

def Undecidability.Host.s2Word : HostWord

The substitution word y⁻¹ * s⁻¹ * y for the eliminated second stable generator.

Equations

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

def Undecidability.Host.tau : OldGen → HostWord

The ordered substitution tau used in the six Tietze eliminations.

Equations

• Undecidability.Host.tau Undecidability.Host.OldGen.d = Undecidability.Host.dWord
• Undecidability.Host.tau Undecidability.Host.OldGen.e = Undecidability.Host.eWord
• Undecidability.Host.tau Undecidability.Host.OldGen.s1 = Undecidability.Host.sWord
• Undecidability.Host.tau Undecidability.Host.OldGen.s2 = Undecidability.Host.s2Word
• Undecidability.Host.tau Undecidability.Host.OldGen.c = Undecidability.Host.cWord
• Undecidability.Host.tau Undecidability.Host.OldGen.t = Undecidability.Host.tWord
• Undecidability.Host.tau Undecidability.Host.OldGen.k = Undecidability.Host.kWord
• Undecidability.Host.tau Undecidability.Host.OldGen.y = Undecidability.Host.yWord
• Undecidability.Host.tau Undecidability.Host.OldGen.z = Undecidability.Host.zWord

def Undecidability.Host.rho (F E : Fin 3 → List (Fin 2)) (P : List (Fin 2)) (i : Fin 9) : HostWord

rhoᵢ is the image under tau of the ith relator in oldSurvivingRelator.

Equations

• Undecidability.Host.rho F E P i = Undecidability.Host.OldWord.evaluate Undecidability.Host.tau (Undecidability.Host.oldSurvivingRelator F E P i)

def Undecidability.Host.presentation (F E : Fin 3 → List (Fin 2)) (P : List (Fin 2)) : FP 3 9

An explicit three-generator, nine-relator presentation of the group in Proposition 2.3 of the paper.

Equations

• Undecidability.Host.presentation F E P = { relator := Undecidability.Host.rho F E P }

def Undecidability.Host.presentationOf (datum : Thue.StandingDatum) : FP 3 9

The three-generator nine-relator host presentation attached to the proved Thue datum.

Equations

• Undecidability.Host.presentationOf datum = Undecidability.Host.presentation datum.F datum.E datum.P

def Undecidability.Host.positiveWord (Q : List (Fin 2)) : HostWord

Evaluate a positive Thue word after tau.

Equations

• Undecidability.Host.positiveWord Q = Undecidability.Word.substitutePositive Undecidability.Host.sWord Undecidability.Host.s2Word Q

def Undecidability.Host.testWord (Q : List (Fin 2)) : HostWord

The compressed image of Borisov's test word [Q⁻¹tQ,k].

Equations

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

theorem Undecidability.Host.testWord_computable : Computable testWord

The syntactic map from a Thue input to the host test word is computable.