Construction

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

@[reducible, inline]

abbrev Undecidability.Borisov.BorisovWord : Type

Words on Borisov’s seven generators d, e, s₁, s₂, c, t, k.

Equations

• Undecidability.Borisov.BorisovWord = Undecidability.Word 7

def Undecidability.Borisov.dWord : BorisovWord

Generator order: d,e,s₁,s₂,c,t,k.

Equations

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

def Undecidability.Borisov.eWord : BorisovWord

The word consisting of the generator e.

Equations

• Undecidability.Borisov.eWord = Undecidability.Word.generator 1

def Undecidability.Borisov.s1Word : BorisovWord

The word consisting of the first stable generator s₁.

Equations

• Undecidability.Borisov.s1Word = Undecidability.Word.generator 2

def Undecidability.Borisov.s2Word : BorisovWord

The word consisting of the second stable generator s₂.

Equations

• Undecidability.Borisov.s2Word = Undecidability.Word.generator 3

def Undecidability.Borisov.cWord : BorisovWord

The word consisting of the generator c.

Equations

• Undecidability.Borisov.cWord = Undecidability.Word.generator 4

def Undecidability.Borisov.tWord : BorisovWord

The word consisting of the generator t.

Equations

• Undecidability.Borisov.tWord = Undecidability.Word.generator 5

def Undecidability.Borisov.kWord : BorisovWord

The word consisting of the generator k.

Equations

• Undecidability.Borisov.kWord = Undecidability.Word.generator 6

def Undecidability.Borisov.positiveWord (w : List (Fin 2)) : BorisovWord

Substitute the two stable-generator words into a positive binary word.

Equations

• Undecidability.Borisov.positiveWord w = Undecidability.Word.substitutePositive Undecidability.Borisov.s1Word Undecidability.Borisov.s2Word w

def Undecidability.Borisov.sDRelator (s : BorisovWord) : BorisovWord

The relator imposing s⁻¹ * d⁴ * s = d.

Equations

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

def Undecidability.Borisov.sERelator (s : BorisovWord) : BorisovWord

The relator imposing s⁻¹ * e * s = e⁴.

Equations

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

def Undecidability.Borisov.simulationRelator (datum : Thue.StandingDatum) (i : Fin 3) : BorisovWord

The relator simulating one indexed binary rewriting rule through conjugation by c.

Equations

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

def Undecidability.Borisov.pWord (datum : Thue.StandingDatum) : BorisovWord

The conjugate of t associated with the fixed target word.

Equations

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

def Undecidability.Borisov.presentation (datum : Thue.StandingDatum) : FP 7 14

Borisov's seven-generator, fourteen-relator simulator Gamma.

Equations

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

def Undecidability.Borisov.testWord (Q : List (Fin 2)) : BorisovWord

Borisov's test word [Q⁻¹tQ,k].

Equations

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

@[simp]

theorem Undecidability.Borisov.eval_positiveWord {G : Type u_1} [Group G] (x : Fin 7 → G) (w : List (Fin 2)) : Word.eval x (positiveWord w) = Thue.evalPositive (x 2) (x 3) w

@[reducible, inline]

abbrev Undecidability.Borisov.gen (datum : Thue.StandingDatum) (i : Fin 7) : (presentation datum).Group

The indicated generator in Borisov’s presented group.

Equations

• Undecidability.Borisov.gen datum i = PresentedGroup.of i

def Undecidability.Borisov.testCommutes (datum : Thue.StandingDatum) (Q : List (Fin 2)) : Prop

The test conjugate of t commutes with k.

Equations

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

theorem Undecidability.Borisov.criterion_forward (datum : Thue.StandingDatum) (Q : List (Fin 2)) : ThueEq (Thue.systemOf datum.F datum.E) Q datum.P → (presentation datum).wordProblem (testWord Q)

The elementary direction of Borisov's simulation theorem. It uses only the defining relators: one Thue rewrite preserves commutation of Q⁻¹tQ with k, and the target relator supplies the base case at P.