The already-verified four-relator HNN model supplies the first two HNN stages. We only have to map its four-generator presentation into the first four generators of Borisov's full presentation.

@[reducible, inline]

abbrev Undecidability.BorisovFinalModelInjective.Presented (datum : Thue.StandingDatum) : Type

The group defined by Borisov’s fourteen-relator presentation.

Equations

• Undecidability.BorisovFinalModelInjective.Presented datum = (Undecidability.Borisov.presentation datum).Group

def Undecidability.BorisovFinalModelInjective.presentedGenerator (datum : Thue.StandingDatum) : Fin 7 → Presented datum

The seven generators of Borisov’s presented group.

Equations

• Undecidability.BorisovFinalModelInjective.presentedGenerator datum = PresentedGroup.of

def Undecidability.BorisovFinalModelInjective.g0Generator (datum : Thue.StandingDatum) : Fin 4 → Presented datum

The four generators of the initial Borisov stage, interpreted in the full presentation.

Equations

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

theorem Undecidability.BorisovFinalModelInjective.g0_relators (datum : Thue.StandingDatum) (r : FreeGroup (Fin 4)) : r ∈ BorisovIntersections.presentation.relSet → (FreeGroup.lift (g0Generator datum)) r = 1

def Undecidability.BorisovFinalModelInjective.g0ToPresented (datum : Thue.StandingDatum) : BorisovIntersections.G0 →* Presented datum

The homomorphism from the initial four-generator presentation to the full presentation.

Equations

• Undecidability.BorisovFinalModelInjective.g0ToPresented datum = PresentedGroup.toGroup ⋯

noncomputable def Undecidability.BorisovFinalModelInjective.gamma3ToPresented (datum : Thue.StandingDatum) : BorisovHNNModel.Gamma3 →* Presented datum

Reverse map from the semantic two-stable-letter group Gamma3 to the full Borisov presentation.

Equations

• Undecidability.BorisovFinalModelInjective.gamma3ToPresented datum = (Undecidability.BorisovFinalModelInjective.g0ToPresented datum).comp Undecidability.BorisovG0HNN.fromHNN

@[simp]

theorem Undecidability.BorisovFinalModelInjective.gamma3ToPresented_d3 (datum : Thue.StandingDatum) : (gamma3ToPresented datum) BorisovHNNModel.d3 = presentedGenerator datum 0

@[simp]

theorem Undecidability.BorisovFinalModelInjective.gamma3ToPresented_e3 (datum : Thue.StandingDatum) : (gamma3ToPresented datum) BorisovHNNModel.e3 = presentedGenerator datum 1

@[simp]

theorem Undecidability.BorisovFinalModelInjective.gamma3ToPresented_s1_3 (datum : Thue.StandingDatum) : (gamma3ToPresented datum) BorisovHNNModel.firstStableInStageThree = presentedGenerator datum 2

@[simp]

theorem Undecidability.BorisovFinalModelInjective.gamma3ToPresented_s2_3 (datum : Thue.StandingDatum) : (gamma3ToPresented datum) BorisovHNNModel.secondStableInStageThree = presentedGenerator datum 3

@[simp]

theorem Undecidability.BorisovFinalModelInjective.gamma3ToPresented_positive3 (datum : Thue.StandingDatum) (w : List (Fin 2)) : (gamma3ToPresented datum) (BorisovCStage.positive3 w) = Thue.evalPositive (presentedGenerator datum 2) (presentedGenerator datum 3) w

theorem Undecidability.BorisovFinalModelInjective.c_lift_condition (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (a : ↥(BorisovCStage.U datum)) : (presentedGenerator datum 4)⁻¹ * (gamma3ToPresented datum) ↑a = (gamma3ToPresented datum) ↑((BorisovCStage.cEquiv datum hfree) a) * (presentedGenerator datum 4)⁻¹

noncomputable def Undecidability.BorisovFinalModelInjective.gamma2ToPresented (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovCStage.Gamma2 datum hfree →* Presented datum

Reverse map through Borisov's c-HNN extension.

Equations

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

@[simp]

theorem Undecidability.BorisovFinalModelInjective.gamma2ToPresented_of3 (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (x : BorisovHNNModel.Gamma3) : (gamma2ToPresented datum hfree) ((BorisovCStage.of3 datum hfree) x) = (gamma3ToPresented datum) x

@[simp]

theorem Undecidability.BorisovFinalModelInjective.gamma2ToPresented_c (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (gamma2ToPresented datum hfree) (BorisovCStage.c datum hfree) = presentedGenerator datum 4

noncomputable def Undecidability.BorisovFinalModelInjective.tStageToPresented (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovConverseCore.TStage datum hfree →* Presented datum

Reverse map through the t centralizer HNN extension.

Equations

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

@[simp]

theorem Undecidability.BorisovFinalModelInjective.tStageToPresented_of (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (x : BorisovCStage.Gamma2 datum hfree) : (tStageToPresented datum hfree) ((BorisovConverseCore.toTStage datum hfree) x) = (gamma2ToPresented datum hfree) x

@[simp]

theorem Undecidability.BorisovFinalModelInjective.tStageToPresented_t (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (tStageToPresented datum hfree) (BorisovConverseCore.tLetter datum hfree) = presentedGenerator datum 5

@[simp]

theorem Undecidability.BorisovFinalModelInjective.gamma2ToPresented_positive2 (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (w : List (Fin 2)) : (gamma2ToPresented datum hfree) (BorisovCStage.positive2 datum hfree w) = Thue.evalPositive (presentedGenerator datum 2) (presentedGenerator datum 3) w

@[simp]

theorem Undecidability.BorisovFinalModelInjective.tStageToPresented_conjugatedT (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (w : List (Fin 2)) : (tStageToPresented datum hfree) (BorisovConverseCore.conjugatedT datum hfree w) = (Thue.evalPositive (presentedGenerator datum 2) (presentedGenerator datum 3) w)⁻¹ * presentedGenerator datum 5 * Thue.evalPositive (presentedGenerator datum 2) (presentedGenerator datum 3) w

noncomputable def Undecidability.BorisovFinalModelInjective.fromFinalModel (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovConverseCore.FinalStage datum hfree →* Presented datum

The complete reverse homomorphism from the semantic final HNN model to Borisov's fourteen-relator presentation.

Equations

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

@[simp]

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_of (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (x : BorisovConverseCore.TStage datum hfree) : (fromFinalModel datum hfree) ((BorisovConverseCore.toFinalStage datum hfree) x) = (tStageToPresented datum hfree) x

@[simp]

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_k (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (fromFinalModel datum hfree) (BorisovConverseCore.kLetter datum hfree) = presentedGenerator datum 6

@[simp]

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_modelD (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (fromFinalModel datum hfree) (BorisovFinalModel.modelD datum hfree) = presentedGenerator datum 0

@[simp]

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_modelE (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (fromFinalModel datum hfree) (BorisovFinalModel.modelE datum hfree) = presentedGenerator datum 1

@[simp]

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_modelS1 (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (fromFinalModel datum hfree) (BorisovFinalModel.modelS1 datum hfree) = presentedGenerator datum 2

@[simp]

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_modelS2 (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (fromFinalModel datum hfree) (BorisovFinalModel.modelS2 datum hfree) = presentedGenerator datum 3

@[simp]

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_modelC (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (fromFinalModel datum hfree) (BorisovFinalModel.modelC datum hfree) = presentedGenerator datum 4

@[simp]

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_modelT (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (fromFinalModel datum hfree) (BorisovFinalModel.modelT datum hfree) = presentedGenerator datum 5

@[simp]

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_modelK (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (fromFinalModel datum hfree) (BorisovFinalModel.modelK datum hfree) = presentedGenerator datum 6

theorem Undecidability.BorisovFinalModelInjective.fromFinalModel_comp_toFinalModel (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : (fromFinalModel datum hfree).comp (BorisovFinalModel.toFinalModel datum hfree) = MonoidHom.id (Presented datum)

theorem Undecidability.BorisovFinalModelInjective.toFinalModel_injective_internal (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Function.Injective ⇑(BorisovFinalModel.toFinalModel datum hfree)

theorem Undecidability.BorisovFinalModel.toFinalModel_injective (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Function.Injective ⇑(toFinalModel datum hfree)

The canonical homomorphism from Borisov's fourteen-relator presentation to its iterated-HNN semantic model is injective. The proof constructs an explicit left inverse through all five HNN stages.