FinalModel

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

noncomputable def Undecidability.BorisovFinalModel.cStageToFinal (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovCStage.Gamma2 datum hfree →* BorisovConverseCore.FinalStage datum hfree

The composite inclusion from the rewriting-rule HNN extension to the final group.

Equations

• Undecidability.BorisovFinalModel.cStageToFinal datum hfree = (Undecidability.BorisovConverseCore.toFinalStage datum hfree).comp (Undecidability.BorisovConverseCore.toTStage datum hfree)

noncomputable def Undecidability.BorisovFinalModel.modelD (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovConverseCore.FinalStage datum hfree

The image of the generator d in the final iterated-HNN model.

Equations

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

noncomputable def Undecidability.BorisovFinalModel.modelE (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovConverseCore.FinalStage datum hfree

The image of the generator e in the final iterated-HNN model.

Equations

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

noncomputable def Undecidability.BorisovFinalModel.modelS1 (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovConverseCore.FinalStage datum hfree

The image of the first stable generator in the final iterated-HNN model.

Equations

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

noncomputable def Undecidability.BorisovFinalModel.modelS2 (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovConverseCore.FinalStage datum hfree

The image of the second stable generator in the final iterated-HNN model.

Equations

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

noncomputable def Undecidability.BorisovFinalModel.modelC (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovConverseCore.FinalStage datum hfree

The image of the rule-transport generator c in the final model.

Equations

• Undecidability.BorisovFinalModel.modelC datum hfree = (Undecidability.BorisovFinalModel.cStageToFinal datum hfree) (Undecidability.BorisovCStage.c datum hfree)

noncomputable def Undecidability.BorisovFinalModel.modelT (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovConverseCore.FinalStage datum hfree

The image of the generator t in the final model.

Equations

• Undecidability.BorisovFinalModel.modelT datum hfree = (Undecidability.BorisovConverseCore.toFinalStage datum hfree) (Undecidability.BorisovConverseCore.tLetter datum hfree)

noncomputable def Undecidability.BorisovFinalModel.modelK (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovConverseCore.FinalStage datum hfree

The final-model generator k.

Equations

• Undecidability.BorisovFinalModel.modelK datum hfree = Undecidability.BorisovConverseCore.kLetter datum hfree

noncomputable def Undecidability.BorisovFinalModel.modelGenerator (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Fin 7 → BorisovConverseCore.FinalStage datum hfree

Generator order d,e,s₁,s₂,c,t,k, matching Borisov.presentation.

Equations

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

@[simp]

theorem Undecidability.BorisovFinalModel.eval_dWord (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Word.eval (modelGenerator datum hfree) Borisov.dWord = modelD datum hfree

@[simp]

theorem Undecidability.BorisovFinalModel.eval_eWord (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Word.eval (modelGenerator datum hfree) Borisov.eWord = modelE datum hfree

@[simp]

theorem Undecidability.BorisovFinalModel.eval_s1Word (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Word.eval (modelGenerator datum hfree) Borisov.s1Word = modelS1 datum hfree

@[simp]

theorem Undecidability.BorisovFinalModel.eval_s2Word (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Word.eval (modelGenerator datum hfree) Borisov.s2Word = modelS2 datum hfree

@[simp]

theorem Undecidability.BorisovFinalModel.eval_cWord (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Word.eval (modelGenerator datum hfree) Borisov.cWord = modelC datum hfree

@[simp]

theorem Undecidability.BorisovFinalModel.eval_tWord (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Word.eval (modelGenerator datum hfree) Borisov.tWord = modelT datum hfree

@[simp]

theorem Undecidability.BorisovFinalModel.eval_kWord (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Word.eval (modelGenerator datum hfree) Borisov.kWord = modelK datum hfree

theorem Undecidability.BorisovFinalModel.eval_positiveWord (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (w : List (Fin 2)) : Word.eval (modelGenerator datum hfree) (Borisov.positiveWord w) = (cStageToFinal datum hfree) (BorisovCStage.positive2 datum hfree w)

theorem Undecidability.BorisovFinalModel.model_relators (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (r : FreeGroup (Fin 7)) : r ∈ (Borisov.presentation datum).relSet → (FreeGroup.lift (modelGenerator datum hfree)) r = 1

noncomputable def Undecidability.BorisovFinalModel.toFinalModel (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (Borisov.presentation datum).Group →* BorisovConverseCore.FinalStage datum hfree

The canonical homomorphism from Borisov's finite presentation to the semantic iterated-HNN model.

Equations

• Undecidability.BorisovFinalModel.toFinalModel datum hfree = PresentedGroup.toGroup ⋯

@[simp]

theorem Undecidability.BorisovFinalModel.toFinalModel_of (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (i : Fin 7) : (toFinalModel datum hfree) (PresentedGroup.of i) = modelGenerator datum hfree i

theorem Undecidability.BorisovFinalModel.toFinalModel_evalWord (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (w : Borisov.BorisovWord) : (toFinalModel datum hfree) ((Borisov.presentation datum).evalWord w) = Word.eval (modelGenerator datum hfree) w

theorem Undecidability.BorisovFinalModel.eval_testWord (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) {Q : List (Fin 2)} : Word.eval (modelGenerator datum hfree) (Borisov.testWord Q) = (BorisovConverseCore.finalConjugatedT datum hfree Q)⁻¹ * (modelK datum hfree)⁻¹ * BorisovConverseCore.finalConjugatedT datum hfree Q * modelK datum hfree

theorem Undecidability.BorisovFinalModel.criterion_converse_of_borisov_inputs (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BorisovContextNormalForm.BaseIntersections datum) (hlemma4 : BorisovCStage.BorisovLemma4 datum hfree) (Q : List (Fin 2)) : (Borisov.presentation datum).wordProblem (Borisov.testWord Q) → ThueEq (Thue.systemOf datum.F datum.E) Q datum.P

Borisov's converse criterion follows from the subgroup intersections and the positive-c pinch induction.