The first compression HNN extension

This file formalizes Lemma 3.1 of the paper and the associated subgroup isomorphism. The ambient group Gamma is the semantic Borisov group. The two associated subgroups are exactly

• HMinus = ⟨d,e,c,t,s₁⟩, and
• HPlus = ⟨d,e,c,k,s₂⟩.

The subgroup isomorphism following Lemma 3.1 defines the proper y-stage and its base embedding. It is constructed below from restricted HNN extensions.

The symmetry between J₁ and J₂

The base change underlying the isomorphism following Lemma 3.1 is already visible before adjoining c: d ↦ e⁻¹, e ↦ d, s₁ ↦ s₂⁻¹. We construct it as an honest automorphism of the four-generator group Gamma3; its inverse sends d ↦ e, e ↦ d⁻¹ and has the same action on the stable letters.

noncomputable def Undecidability.HostYStage.twistGenerator : Fin 4 → BorisovHNNModel.Gamma3

The four generator images defining the twisting automorphism of the initial Borisov group.

Equations

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

noncomputable def Undecidability.HostYStage.untwistGenerator : Fin 4 → BorisovHNNModel.Gamma3

The four generator images defining the inverse twisting automorphism.

Equations

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

theorem Undecidability.HostYStage.twist_relators (r : FreeGroup (Fin 4)) : r ∈ BorisovIntersections.presentation.relSet → (FreeGroup.lift twistGenerator) r = 1

theorem Undecidability.HostYStage.untwist_relators (r : FreeGroup (Fin 4)) : r ∈ BorisovIntersections.presentation.relSet → (FreeGroup.lift untwistGenerator) r = 1

noncomputable def Undecidability.HostYStage.twistFromG0 : BorisovIntersections.G0 →* BorisovHNNModel.Gamma3

The twist interpreted as a homomorphism from the initial Borisov presentation.

Equations

• Undecidability.HostYStage.twistFromG0 = PresentedGroup.toGroup Undecidability.HostYStage.twist_relators

noncomputable def Undecidability.HostYStage.untwistFromG0 : BorisovIntersections.G0 →* BorisovHNNModel.Gamma3

The inverse twist interpreted as a homomorphism from the initial presentation.

Equations

• Undecidability.HostYStage.untwistFromG0 = PresentedGroup.toGroup Undecidability.HostYStage.untwist_relators

noncomputable def Undecidability.HostYStage.twistHom : BorisovHNNModel.Gamma3 →* BorisovHNNModel.Gamma3

The twisting endomorphism of the two-HNN-extension model.

Equations

• Undecidability.HostYStage.twistHom = Undecidability.HostYStage.twistFromG0.comp Undecidability.BorisovG0HNN.g0Equiv.symm.toMonoidHom

noncomputable def Undecidability.HostYStage.untwistHom : BorisovHNNModel.Gamma3 →* BorisovHNNModel.Gamma3

The inverse twisting endomorphism of the two-HNN-extension model.

Equations

• Undecidability.HostYStage.untwistHom = Undecidability.HostYStage.untwistFromG0.comp Undecidability.BorisovG0HNN.g0Equiv.symm.toMonoidHom

@[simp]

theorem Undecidability.HostYStage.twistHom_d3 : twistHom BorisovHNNModel.d3 = BorisovHNNModel.e3⁻¹

@[simp]

theorem Undecidability.HostYStage.twistHom_e3 : twistHom BorisovHNNModel.e3 = BorisovHNNModel.d3

@[simp]

theorem Undecidability.HostYStage.twistHom_s1_3 : twistHom BorisovHNNModel.firstStableInStageThree = BorisovHNNModel.secondStableInStageThree⁻¹

@[simp]

theorem Undecidability.HostYStage.twistHom_s2_3 : twistHom BorisovHNNModel.secondStableInStageThree = BorisovHNNModel.firstStableInStageThree⁻¹

@[simp]

theorem Undecidability.HostYStage.untwistHom_d3 : untwistHom BorisovHNNModel.d3 = BorisovHNNModel.e3

@[simp]

theorem Undecidability.HostYStage.untwistHom_e3 : untwistHom BorisovHNNModel.e3 = BorisovHNNModel.d3⁻¹

@[simp]

theorem Undecidability.HostYStage.untwistHom_s1_3 : untwistHom BorisovHNNModel.firstStableInStageThree = BorisovHNNModel.secondStableInStageThree⁻¹

@[simp]

theorem Undecidability.HostYStage.untwistHom_s2_3 : untwistHom BorisovHNNModel.secondStableInStageThree = BorisovHNNModel.firstStableInStageThree⁻¹

theorem Undecidability.HostYStage.untwist_comp_twist : untwistHom.comp twistHom = MonoidHom.id BorisovHNNModel.Gamma3

theorem Undecidability.HostYStage.twist_comp_untwist : twistHom.comp untwistHom = MonoidHom.id BorisovHNNModel.Gamma3

theorem Undecidability.HostYStage.twist_mem_J3 {x : BorisovHNNModel.Gamma3} (hx : x ∈ BorisovInputsBridge.J3 0) : twistHom x ∈ BorisovInputsBridge.J3 1

theorem Undecidability.HostYStage.untwist_mem_J3 {x : BorisovHNNModel.Gamma3} (hx : x ∈ BorisovInputsBridge.J3 1) : untwistHom x ∈ BorisovInputsBridge.J3 0

noncomputable def Undecidability.HostYStage.jEquiv : ↥(BorisovInputsBridge.J3 0) ≃* ↥(BorisovInputsBridge.J3 1)

The base isomorphism J₁ ≃ J₂ used by the restricted c-HNN extensions.

Equations

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

theorem Undecidability.HostYStage.twist_mem_U (datum : Thue.StandingDatum) {x : BorisovHNNModel.Gamma3} (hxU : x ∈ BorisovCStage.U datum) (hxJ : x ∈ BorisovInputsBridge.J3 0) : twistHom x ∈ BorisovCStage.U datum

theorem Undecidability.HostYStage.untwist_mem_U (datum : Thue.StandingDatum) {x : BorisovHNNModel.Gamma3} (hxU : x ∈ BorisovCStage.U datum) (hxJ : x ∈ BorisovInputsBridge.J3 1) : untwistHom x ∈ BorisovCStage.U datum

theorem Undecidability.HostYStage.twist_mem_V (datum : Thue.StandingDatum) {x : BorisovHNNModel.Gamma3} (hxV : x ∈ BorisovCStage.V datum) (hxJ : x ∈ BorisovInputsBridge.J3 0) : twistHom x ∈ BorisovCStage.V datum

theorem Undecidability.HostYStage.untwist_mem_V (datum : Thue.StandingDatum) {x : BorisovHNNModel.Gamma3} (hxV : x ∈ BorisovCStage.V datum) (hxJ : x ∈ BorisovInputsBridge.J3 1) : untwistHom x ∈ BorisovCStage.V datum

@[reducible, inline]

noncomputable abbrev Undecidability.HostYStage.CRestrictedA (datum : Thue.StandingDatum) (beta : Fin 2) : Subgroup ↥(BorisovInputsBridge.J3 beta)

The source rule subgroup restricted to the selected three-generator subgroup.

Equations

• Undecidability.HostYStage.CRestrictedA datum beta = Undecidability.HNNLemmas.restrictedA (Undecidability.BorisovInputsBridge.J3 beta)

@[reducible, inline]

noncomputable abbrev Undecidability.HostYStage.CRestrictedB (datum : Thue.StandingDatum) (beta : Fin 2) : Subgroup ↥(BorisovInputsBridge.J3 beta)

The target rule subgroup restricted to the selected three-generator subgroup.

Equations

• Undecidability.HostYStage.CRestrictedB datum beta = Undecidability.HNNLemmas.restrictedB (Undecidability.BorisovInputsBridge.J3 beta)

noncomputable def Undecidability.HostYStage.cRestrictedPhi (datum : Thue.StandingDatum) (beta : Fin 2) : ↥(CRestrictedA datum beta) ≃* ↥(CRestrictedB datum beta)

The rewriting-rule subgroup isomorphism restricted to the selected base subgroup.

Equations

• Undecidability.HostYStage.cRestrictedPhi datum beta = Undecidability.HNNLemmas.restrictedPhi (Undecidability.BorisovInputsBridge.J3 beta) ⋯

@[reducible, inline]

abbrev Undecidability.HostYStage.CRestricted (datum : Thue.StandingDatum) (beta : Fin 2) : Type

The exact restricted c-HNN extension over J_beta.

Equations

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

noncomputable def Undecidability.HostYStage.cRestrictedAEquiv (datum : Thue.StandingDatum) : ↥(CRestrictedA datum 0) ≃* ↥(CRestrictedA datum 1)

The twisting equivalence between the two restricted source rule subgroups.

Equations

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

noncomputable def Undecidability.HostYStage.cRestrictedBEquiv (datum : Thue.StandingDatum) : ↥(CRestrictedB datum 0) ≃* ↥(CRestrictedB datum 1)

The twisting equivalence between the two restricted target rule subgroups.

Equations

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

theorem Undecidability.HostYStage.cRestricted_intertwines (datum : Thue.StandingDatum) (a : ↥(CRestrictedA datum 0)) : (cRestrictedBEquiv datum) ((cRestrictedPhi datum 0) a) = (cRestrictedPhi datum 1) ((cRestrictedAEquiv datum) a)

noncomputable def Undecidability.HostYStage.cRestrictedEquiv (datum : Thue.StandingDatum) : CRestricted datum 0 ≃* CRestricted datum 1

The exact c-stage symmetry, obtained by transporting both restricted associated subgroups along jEquiv.

Equations

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

noncomputable def Undecidability.HostYStage.CSubgroup (datum : Thue.StandingDatum) (beta : Fin 2) : Subgroup (BorisovCStage.Gamma2 datum ⋯)

The exact subgroup ⟨d,e,c,s_beta⟩ of Gamma2.

Equations

• Undecidability.HostYStage.CSubgroup datum beta = Undecidability.HNNLemmas.generatedWithStable (Undecidability.BorisovInputsBridge.J3 beta)

noncomputable def Undecidability.HostYStage.cRestrictedRangeEquiv (datum : Thue.StandingDatum) (beta : Fin 2) : CRestricted datum beta ≃* ↥(CSubgroup datum beta)

The equivalence from the restricted HNN model onto its generated subgroup.

Equations

• Undecidability.HostYStage.cRestrictedRangeEquiv datum beta = Undecidability.HNNLemmas.restrictedEquivGeneratedWithStable (Undecidability.BorisovInputsBridge.J3 beta) ⋯

noncomputable def Undecidability.HostYStage.cSubgroupEquiv (datum : Thue.StandingDatum) : ↥(CSubgroup datum 0) ≃* ↥(CSubgroup datum 1)

The induced isomorphism ⟨d,e,c,s₁⟩ ≃ ⟨d,e,c,s₂⟩.

Equations

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

theorem Undecidability.HostYStage.d3_mem_J3 (beta : Fin 2) : BorisovHNNModel.d3 ∈ BorisovInputsBridge.J3 beta

theorem Undecidability.HostYStage.e3_mem_J3 (beta : Fin 2) : BorisovHNNModel.e3 ∈ BorisovInputsBridge.J3 beta

theorem Undecidability.HostYStage.stable3_mem_J3 (beta : Fin 2) : BorisovCStage.stable3 beta ∈ BorisovInputsBridge.J3 beta

noncomputable def Undecidability.HostYStage.coreD (datum : Thue.StandingDatum) (beta : Fin 2) : ↥(CSubgroup datum beta)

The generator d regarded as an element of the selected core subgroup.

Equations

• Undecidability.HostYStage.coreD datum beta = ⟨(Undecidability.BorisovCStage.of3 datum ⋯) Undecidability.BorisovHNNModel.d3, ⋯⟩

noncomputable def Undecidability.HostYStage.coreE (datum : Thue.StandingDatum) (beta : Fin 2) : ↥(CSubgroup datum beta)

The generator e regarded as an element of the selected core subgroup.

Equations

• Undecidability.HostYStage.coreE datum beta = ⟨(Undecidability.BorisovCStage.of3 datum ⋯) Undecidability.BorisovHNNModel.e3, ⋯⟩

noncomputable def Undecidability.HostYStage.coreStable (datum : Thue.StandingDatum) (beta : Fin 2) : ↥(CSubgroup datum beta)

The selected stable generator regarded as an element of the core subgroup.

Equations

• Undecidability.HostYStage.coreStable datum beta = ⟨(Undecidability.BorisovCStage.of3 datum ⋯) (Undecidability.BorisovCStage.stable3 beta), ⋯⟩

noncomputable def Undecidability.HostYStage.coreC (datum : Thue.StandingDatum) (beta : Fin 2) : ↥(CSubgroup datum beta)

The generator c regarded as an element of the core subgroup.

Equations

• Undecidability.HostYStage.coreC datum beta = ⟨Undecidability.BorisovCStage.c datum ⋯, ⋯⟩

@[simp]

theorem Undecidability.HostYStage.cSubgroupEquiv_coreD (datum : Thue.StandingDatum) : (cSubgroupEquiv datum) (coreD datum 0) = (coreE datum 1)⁻¹

@[simp]

theorem Undecidability.HostYStage.cSubgroupEquiv_coreE (datum : Thue.StandingDatum) : (cSubgroupEquiv datum) (coreE datum 0) = coreD datum 1

@[simp]

theorem Undecidability.HostYStage.cSubgroupEquiv_coreC (datum : Thue.StandingDatum) : (cSubgroupEquiv datum) (coreC datum 0) = coreC datum 1

@[simp]

theorem Undecidability.HostYStage.cSubgroupEquiv_coreS1 (datum : Thue.StandingDatum) : (cSubgroupEquiv datum) (coreStable datum 0) = (coreStable datum 1)⁻¹

theorem Undecidability.HostYStage.cSubgroupEquiv_mem_CD_iff (datum : Thue.StandingDatum) (x : ↥(CSubgroup datum 0)) : ↑x ∈ BorisovCStage.CD datum ⋯ ↔ ↑((cSubgroupEquiv datum) x) ∈ BorisovCStage.CE datum ⋯

The outer t/k restricted HNN extensions

theorem Undecidability.HostYStage.toTStage_injective (datum : Thue.StandingDatum) : Function.Injective ⇑(BorisovConverseCore.toTStage datum ⋯)

noncomputable def Undecidability.HostYStage.PlusBase (datum : Thue.StandingDatum) : Subgroup (BorisovConverseCore.TStage datum ⋯)

The plus-side four-generator base, embedded in the t-stage.

Equations

• Undecidability.HostYStage.PlusBase datum = Subgroup.map (Undecidability.BorisovConverseCore.toTStage datum ⋯) (Undecidability.HostYStage.CSubgroup datum 1)

noncomputable def Undecidability.HostYStage.cSubgroupToPlusBase (datum : Thue.StandingDatum) : ↥(CSubgroup datum 1) ≃* ↥(PlusBase datum)

The equivalence carrying the positive core subgroup into the final-stage base group.

Equations

• Undecidability.HostYStage.cSubgroupToPlusBase datum = (Undecidability.HostYStage.CSubgroup datum 1).equivMapOfInjective (Undecidability.BorisovConverseCore.toTStage datum ⋯) ⋯

noncomputable def Undecidability.HostYStage.outerBaseEquiv (datum : Thue.StandingDatum) : ↥(CSubgroup datum 0) ≃* ↥(PlusBase datum)

The base equivalence for the outer HNN congruence.

Equations

• Undecidability.HostYStage.outerBaseEquiv datum = (Undecidability.HostYStage.cSubgroupEquiv datum).trans (Undecidability.HostYStage.cSubgroupToPlusBase datum)

@[simp]

theorem Undecidability.HostYStage.outerBaseEquiv_coe (datum : Thue.StandingDatum) (x : ↥(CSubgroup datum 0)) : ↑((outerBaseEquiv datum) x) = (BorisovConverseCore.toTStage datum ⋯) ↑((cSubgroupEquiv datum) x)

theorem Undecidability.HostYStage.outerBaseEquiv_mem_associated_iff (datum : Thue.StandingDatum) (x : ↥(CSubgroup datum 0)) : ↑x ∈ BorisovCStage.CD datum ⋯ ↔ ↑((outerBaseEquiv datum) x) ∈ BorisovConverseCore.KSubgroup datum ⋯

theorem Undecidability.HostYStage.minusCompatibility (datum : Thue.StandingDatum) (a : ↥(BorisovCStage.CD datum ⋯)) : ↑a ∈ CSubgroup datum 0 ↔ ↑((MulEquiv.refl ↥(BorisovCStage.CD datum ⋯)) a) ∈ CSubgroup datum 0

theorem Undecidability.HostYStage.plusCompatibility (datum : Thue.StandingDatum) (a : ↥(BorisovConverseCore.KSubgroup datum ⋯)) : ↑a ∈ PlusBase datum ↔ ↑((MulEquiv.refl ↥(BorisovConverseCore.KSubgroup datum ⋯)) a) ∈ PlusBase datum

@[reducible, inline]

noncomputable abbrev Undecidability.HostYStage.MinusA (datum : Thue.StandingDatum) : Subgroup ↥(CSubgroup datum 0)

The first centralizer-associated subgroup restricted to the negative core subgroup.

Equations

• Undecidability.HostYStage.MinusA datum = Undecidability.HNNLemmas.restrictedA (Undecidability.HostYStage.CSubgroup datum 0)

@[reducible, inline]

noncomputable abbrev Undecidability.HostYStage.MinusB (datum : Thue.StandingDatum) : Subgroup ↥(CSubgroup datum 0)

The second centralizer-associated subgroup restricted to the negative core subgroup.

Equations

• Undecidability.HostYStage.MinusB datum = Undecidability.HNNLemmas.restrictedB (Undecidability.HostYStage.CSubgroup datum 0)

noncomputable def Undecidability.HostYStage.minusPhi (datum : Thue.StandingDatum) : ↥(MinusA datum) ≃* ↥(MinusB datum)

The centralizer-subgroup isomorphism restricted to the negative core subgroup.

Equations

• Undecidability.HostYStage.minusPhi datum = Undecidability.HNNLemmas.restrictedPhi (Undecidability.HostYStage.CSubgroup datum 0) ⋯

@[reducible, inline]

abbrev Undecidability.HostYStage.MinusRestricted (datum : Thue.StandingDatum) : Type

Exact parameter group for ⟨d,e,c,t,s₁⟩ before its inclusion in the final k-stage.

Equations

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

@[reducible, inline]

noncomputable abbrev Undecidability.HostYStage.PlusA (datum : Thue.StandingDatum) : Subgroup ↥(PlusBase datum)

The first final-stage associated subgroup restricted to the positive base subgroup.

Equations

• Undecidability.HostYStage.PlusA datum = Undecidability.HNNLemmas.restrictedA (Undecidability.HostYStage.PlusBase datum)

@[reducible, inline]

noncomputable abbrev Undecidability.HostYStage.PlusB (datum : Thue.StandingDatum) : Subgroup ↥(PlusBase datum)

The second final-stage associated subgroup restricted to the positive base subgroup.

Equations

• Undecidability.HostYStage.PlusB datum = Undecidability.HNNLemmas.restrictedB (Undecidability.HostYStage.PlusBase datum)

noncomputable def Undecidability.HostYStage.plusPhi (datum : Thue.StandingDatum) : ↥(PlusA datum) ≃* ↥(PlusB datum)

The final-stage associated-subgroup isomorphism restricted to the positive base.

Equations

• Undecidability.HostYStage.plusPhi datum = Undecidability.HNNLemmas.restrictedPhi (Undecidability.HostYStage.PlusBase datum) ⋯

@[reducible, inline]

abbrev Undecidability.HostYStage.PlusRestricted (datum : Thue.StandingDatum) : Type

Exact parameter group for ⟨d,e,c,k,s₂⟩.

Equations

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

noncomputable def Undecidability.HostYStage.outerAssociatedEquiv (datum : Thue.StandingDatum) : ↥(MinusA datum) ≃* ↥(PlusA datum)

The equivalence of the outer associated subgroups induced by the twisting base equivalence.

Equations

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

theorem Undecidability.HostYStage.outerRestricted_intertwines (datum : Thue.StandingDatum) (a : ↥(MinusA datum)) : (outerAssociatedEquiv datum) ((minusPhi datum) a) = (plusPhi datum) ((outerAssociatedEquiv datum) a)

noncomputable def Undecidability.HostYStage.outerRestrictedEquiv (datum : Thue.StandingDatum) : MinusRestricted datum ≃* PlusRestricted datum

The isomorphism of the exact restricted outer HNN extensions, fixing the stable-letter orientation (t ↦ k).

Equations

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

noncomputable def Undecidability.HostYStage.minusEmbeddingToT (datum : Thue.StandingDatum) : MinusRestricted datum →* BorisovConverseCore.TStage datum ⋯

The embedding of the negative restricted model into the t HNN stage.

Equations

• Undecidability.HostYStage.minusEmbeddingToT datum = Undecidability.HNNLemmas.restrictedEmbedding (Undecidability.HostYStage.CSubgroup datum 0) ⋯

noncomputable def Undecidability.HostYStage.plusEmbedding (datum : Thue.StandingDatum) : PlusRestricted datum →* BorisovConverseCore.FinalStage datum ⋯

The embedding of the positive restricted model into the final HNN stage.

Equations

• Undecidability.HostYStage.plusEmbedding datum = Undecidability.HNNLemmas.restrictedEmbedding (Undecidability.HostYStage.PlusBase datum) ⋯

noncomputable def Undecidability.HostYStage.minusEmbedding (datum : Thue.StandingDatum) : MinusRestricted datum →* BorisovConverseCore.FinalStage datum ⋯

The embedding of the negative restricted model carried into the final HNN stage.

Equations

• Undecidability.HostYStage.minusEmbedding datum = (Undecidability.BorisovConverseCore.toFinalStage datum ⋯).comp (Undecidability.HostYStage.minusEmbeddingToT datum)

@[reducible, inline]

abbrev Undecidability.HostYStage.FreeInput (datum : Thue.StandingDatum) : BorisovCStage.RankFiveFree datum

The proved freeness witness supplying the concrete iterated-HNN model.

Equations

• ⋯ = ⋯

@[reducible, inline]

abbrev Undecidability.HostYStage.Gamma (datum : Thue.StandingDatum) : Type

The semantic Borisov group Gamma.

Equations

• Undecidability.HostYStage.Gamma datum = Undecidability.BorisovConverseCore.FinalStage datum ⋯

noncomputable def Undecidability.HostYStage.d (datum : Thue.StandingDatum) : Gamma datum

The concrete generator d in the final Borisov model.

Equations

• Undecidability.HostYStage.d datum = Undecidability.BorisovFinalModel.modelD datum ⋯

noncomputable def Undecidability.HostYStage.e (datum : Thue.StandingDatum) : Gamma datum

The concrete generator e in the final Borisov model.

Equations

• Undecidability.HostYStage.e datum = Undecidability.BorisovFinalModel.modelE datum ⋯

noncomputable def Undecidability.HostYStage.s1 (datum : Thue.StandingDatum) : Gamma datum

The concrete first stable generator in the final Borisov model.

Equations

• Undecidability.HostYStage.s1 datum = Undecidability.BorisovFinalModel.modelS1 datum ⋯

noncomputable def Undecidability.HostYStage.s2 (datum : Thue.StandingDatum) : Gamma datum

The concrete second stable generator in the final Borisov model.

Equations

• Undecidability.HostYStage.s2 datum = Undecidability.BorisovFinalModel.modelS2 datum ⋯

noncomputable def Undecidability.HostYStage.c (datum : Thue.StandingDatum) : Gamma datum

The concrete generator c in the final Borisov model.

Equations

• Undecidability.HostYStage.c datum = Undecidability.BorisovFinalModel.modelC datum ⋯

noncomputable def Undecidability.HostYStage.t (datum : Thue.StandingDatum) : Gamma datum

The concrete generator t in the final Borisov model.

Equations

• Undecidability.HostYStage.t datum = Undecidability.BorisovFinalModel.modelT datum ⋯

noncomputable def Undecidability.HostYStage.k (datum : Thue.StandingDatum) : Gamma datum

The concrete generator k in the final Borisov model.

Equations

• Undecidability.HostYStage.k datum = Undecidability.BorisovFinalModel.modelK datum ⋯

noncomputable def Undecidability.HostYStage.HMinus (datum : Thue.StandingDatum) : Subgroup (Gamma datum)

H_y^- = ⟨d,e,c,t,s₁⟩.

Equations

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

noncomputable def Undecidability.HostYStage.HPlus (datum : Thue.StandingDatum) : Subgroup (Gamma datum)

H_y^+ = ⟨d,e,c,k,s₂⟩.

Equations

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

@[simp]

theorem Undecidability.HostYStage.d_mem_HMinus (datum : Thue.StandingDatum) : d datum ∈ HMinus datum

@[simp]

theorem Undecidability.HostYStage.e_mem_HMinus (datum : Thue.StandingDatum) : e datum ∈ HMinus datum

@[simp]

theorem Undecidability.HostYStage.c_mem_HMinus (datum : Thue.StandingDatum) : c datum ∈ HMinus datum

@[simp]

theorem Undecidability.HostYStage.t_mem_HMinus (datum : Thue.StandingDatum) : t datum ∈ HMinus datum

@[simp]

theorem Undecidability.HostYStage.s1_mem_HMinus (datum : Thue.StandingDatum) : s1 datum ∈ HMinus datum

@[simp]

theorem Undecidability.HostYStage.d_mem_HPlus (datum : Thue.StandingDatum) : d datum ∈ HPlus datum

@[simp]

theorem Undecidability.HostYStage.e_mem_HPlus (datum : Thue.StandingDatum) : e datum ∈ HPlus datum

@[simp]

theorem Undecidability.HostYStage.c_mem_HPlus (datum : Thue.StandingDatum) : c datum ∈ HPlus datum

@[simp]

theorem Undecidability.HostYStage.k_mem_HPlus (datum : Thue.StandingDatum) : k datum ∈ HPlus datum

@[simp]

theorem Undecidability.HostYStage.s2_mem_HPlus (datum : Thue.StandingDatum) : s2 datum ∈ HPlus datum

noncomputable def Undecidability.HostYStage.MinusGenerated (datum : Thue.StandingDatum) : Subgroup (BorisovConverseCore.TStage datum ⋯)

The generated subgroup on the minus side, still inside the t-stage.

Equations

• Undecidability.HostYStage.MinusGenerated datum = Undecidability.HNNLemmas.generatedWithStable (Undecidability.HostYStage.CSubgroup datum 0)

noncomputable def Undecidability.HostYStage.PlusGenerated (datum : Thue.StandingDatum) : Subgroup (Gamma datum)

The generated subgroup on the plus side, inside the final k-stage.

Equations

• Undecidability.HostYStage.PlusGenerated datum = Undecidability.HNNLemmas.generatedWithStable (Undecidability.HostYStage.PlusBase datum)

noncomputable def Undecidability.HostYStage.minusRestrictedRangeEquiv (datum : Thue.StandingDatum) : MinusRestricted datum ≃* ↥(MinusGenerated datum)

The equivalence from the negative restricted HNN model onto its generated subgroup.

Equations

• Undecidability.HostYStage.minusRestrictedRangeEquiv datum = Undecidability.HNNLemmas.restrictedEquivGeneratedWithStable (Undecidability.HostYStage.CSubgroup datum 0) ⋯

noncomputable def Undecidability.HostYStage.plusRestrictedRangeEquiv (datum : Thue.StandingDatum) : PlusRestricted datum ≃* ↥(PlusGenerated datum)

The equivalence from the positive restricted HNN model onto its generated subgroup.

Equations

• Undecidability.HostYStage.plusRestrictedRangeEquiv datum = Undecidability.HNNLemmas.restrictedEquivGeneratedWithStable (Undecidability.HostYStage.PlusBase datum) ⋯

theorem Undecidability.HostYStage.MinusGenerated_map_eq_HMinus (datum : Thue.StandingDatum) : Subgroup.map (BorisovConverseCore.toFinalStage datum ⋯) (MinusGenerated datum) = HMinus datum

theorem Undecidability.HostYStage.PlusGenerated_eq_HPlus (datum : Thue.StandingDatum) : PlusGenerated datum = HPlus datum

noncomputable def Undecidability.HostYStage.minusGeneratedToImage (datum : Thue.StandingDatum) : ↥(MinusGenerated datum) ≃* ↥(Subgroup.map (BorisovConverseCore.toFinalStage datum ⋯) (MinusGenerated datum))

The equivalence onto the image of the negative generated subgroup in the final stage.

Equations

• Undecidability.HostYStage.minusGeneratedToImage datum = (Undecidability.HostYStage.MinusGenerated datum).equivMapOfInjective (Undecidability.BorisovConverseCore.toFinalStage datum ⋯) ⋯

noncomputable def Undecidability.HostYStage.minusParamEquiv (datum : Thue.StandingDatum) : MinusRestricted datum ≃* ↥(HMinus datum)

Exact parametrization of HMinus.

Equations

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

noncomputable def Undecidability.HostYStage.plusParamEquiv (datum : Thue.StandingDatum) : PlusRestricted datum ≃* ↥(HPlus datum)

Exact parametrization of HPlus.

Equations

• Undecidability.HostYStage.plusParamEquiv datum = (Undecidability.HostYStage.plusRestrictedRangeEquiv datum).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem Undecidability.HostYStage.minusParamEquiv_coe (datum : Thue.StandingDatum) (x : MinusRestricted datum) : ↑((minusParamEquiv datum) x) = (minusEmbedding datum) x

@[simp]

theorem Undecidability.HostYStage.plusParamEquiv_coe (datum : Thue.StandingDatum) (x : PlusRestricted datum) : ↑((plusParamEquiv datum) x) = (plusEmbedding datum) x

noncomputable def Undecidability.HostYStage.minusParamD (datum : Thue.StandingDatum) : MinusRestricted datum

The generator d in the negative restricted model.

Equations

• Undecidability.HostYStage.minusParamD datum = HNNExtension.of (Undecidability.HostYStage.coreD datum 0)

noncomputable def Undecidability.HostYStage.minusParamE (datum : Thue.StandingDatum) : MinusRestricted datum

The generator e in the negative restricted model.

Equations

• Undecidability.HostYStage.minusParamE datum = HNNExtension.of (Undecidability.HostYStage.coreE datum 0)

noncomputable def Undecidability.HostYStage.minusParamC (datum : Thue.StandingDatum) : MinusRestricted datum

The generator c in the negative restricted model.

Equations

• Undecidability.HostYStage.minusParamC datum = HNNExtension.of (Undecidability.HostYStage.coreC datum 0)

noncomputable def Undecidability.HostYStage.minusParamS1 (datum : Thue.StandingDatum) : MinusRestricted datum

The first stable generator in the negative restricted model.

Equations

• Undecidability.HostYStage.minusParamS1 datum = HNNExtension.of (Undecidability.HostYStage.coreStable datum 0)

noncomputable def Undecidability.HostYStage.minusParamT (datum : Thue.StandingDatum) : MinusRestricted datum

The centralizing stable generator t in the negative restricted model.

Equations

• Undecidability.HostYStage.minusParamT datum = HNNExtension.t

noncomputable def Undecidability.HostYStage.plusParamD (datum : Thue.StandingDatum) : PlusRestricted datum

The generator d in the positive restricted model.

Equations

• Undecidability.HostYStage.plusParamD datum = HNNExtension.of ((Undecidability.HostYStage.cSubgroupToPlusBase datum) (Undecidability.HostYStage.coreD datum 1))

noncomputable def Undecidability.HostYStage.plusParamE (datum : Thue.StandingDatum) : PlusRestricted datum

The generator e in the positive restricted model.

Equations

• Undecidability.HostYStage.plusParamE datum = HNNExtension.of ((Undecidability.HostYStage.cSubgroupToPlusBase datum) (Undecidability.HostYStage.coreE datum 1))

noncomputable def Undecidability.HostYStage.plusParamC (datum : Thue.StandingDatum) : PlusRestricted datum

The generator c in the positive restricted model.

Equations

• Undecidability.HostYStage.plusParamC datum = HNNExtension.of ((Undecidability.HostYStage.cSubgroupToPlusBase datum) (Undecidability.HostYStage.coreC datum 1))

noncomputable def Undecidability.HostYStage.plusParamS2 (datum : Thue.StandingDatum) : PlusRestricted datum

The second stable generator in the positive restricted model.

Equations

• Undecidability.HostYStage.plusParamS2 datum = HNNExtension.of ((Undecidability.HostYStage.cSubgroupToPlusBase datum) (Undecidability.HostYStage.coreStable datum 1))

noncomputable def Undecidability.HostYStage.plusParamK (datum : Thue.StandingDatum) : PlusRestricted datum

The stable generator k in the positive restricted model.

Equations

• Undecidability.HostYStage.plusParamK datum = HNNExtension.t

noncomputable def Undecidability.HostYStage.minusD (datum : Thue.StandingDatum) : ↥(HMinus datum)

The element d with its membership witness in the negative associated subgroup.

Equations

• Undecidability.HostYStage.minusD datum = ⟨Undecidability.HostYStage.d datum, ⋯⟩

noncomputable def Undecidability.HostYStage.minusE (datum : Thue.StandingDatum) : ↥(HMinus datum)

The element e with its membership witness in the negative associated subgroup.

Equations

• Undecidability.HostYStage.minusE datum = ⟨Undecidability.HostYStage.e datum, ⋯⟩

noncomputable def Undecidability.HostYStage.minusC (datum : Thue.StandingDatum) : ↥(HMinus datum)

The element c with its membership witness in the negative associated subgroup.

Equations

• Undecidability.HostYStage.minusC datum = ⟨Undecidability.HostYStage.c datum, ⋯⟩

noncomputable def Undecidability.HostYStage.minusT (datum : Thue.StandingDatum) : ↥(HMinus datum)

The element t with its membership witness in the negative associated subgroup.

Equations

• Undecidability.HostYStage.minusT datum = ⟨Undecidability.HostYStage.t datum, ⋯⟩

noncomputable def Undecidability.HostYStage.minusS1 (datum : Thue.StandingDatum) : ↥(HMinus datum)

The first stable element with its membership witness in the negative associated subgroup.

Equations

• Undecidability.HostYStage.minusS1 datum = ⟨Undecidability.HostYStage.s1 datum, ⋯⟩

noncomputable def Undecidability.HostYStage.plusD (datum : Thue.StandingDatum) : ↥(HPlus datum)

The element d with its membership witness in the positive associated subgroup.

Equations

• Undecidability.HostYStage.plusD datum = ⟨Undecidability.HostYStage.d datum, ⋯⟩

noncomputable def Undecidability.HostYStage.plusE (datum : Thue.StandingDatum) : ↥(HPlus datum)

The element e with its membership witness in the positive associated subgroup.

Equations

• Undecidability.HostYStage.plusE datum = ⟨Undecidability.HostYStage.e datum, ⋯⟩

noncomputable def Undecidability.HostYStage.plusC (datum : Thue.StandingDatum) : ↥(HPlus datum)

The element c with its membership witness in the positive associated subgroup.

Equations

• Undecidability.HostYStage.plusC datum = ⟨Undecidability.HostYStage.c datum, ⋯⟩

noncomputable def Undecidability.HostYStage.plusK (datum : Thue.StandingDatum) : ↥(HPlus datum)

The element k with its membership witness in the positive associated subgroup.

Equations

• Undecidability.HostYStage.plusK datum = ⟨Undecidability.HostYStage.k datum, ⋯⟩

noncomputable def Undecidability.HostYStage.plusS2 (datum : Thue.StandingDatum) : ↥(HPlus datum)

The second stable element with its membership witness in the positive associated subgroup.

Equations

• Undecidability.HostYStage.plusS2 datum = ⟨Undecidability.HostYStage.s2 datum, ⋯⟩

structure Undecidability.HostYStage.ThetaData (datum : Thue.StandingDatum) : Type

The output interface of the subgroup isomorphism following Lemma 3.1.

• equiv : ↥(HMinus datum) ≃* ↥(HPlus datum)

  The associated-subgroup isomorphism satisfying the displayed generator images.

• map_d : self.equiv (minusD datum) = (plusE datum)⁻¹
• map_e : self.equiv (minusE datum) = plusD datum
• map_c : self.equiv (minusC datum) = plusC datum
• map_t : self.equiv (minusT datum) = plusK datum
• map_s1 : self.equiv (minusS1 datum) = (plusS2 datum)⁻¹

noncomputable def Undecidability.HostYStage.thetaEquiv (datum : Thue.StandingDatum) : ↥(HMinus datum) ≃* ↥(HPlus datum)

The subgroup isomorphism following Lemma 3.1, constructed from the two exact restricted-HNN parametrizations.

Equations

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

@[simp]

theorem Undecidability.HostYStage.thetaEquiv_minusD (datum : Thue.StandingDatum) : (thetaEquiv datum) (minusD datum) = (plusE datum)⁻¹

@[simp]

theorem Undecidability.HostYStage.thetaEquiv_minusE (datum : Thue.StandingDatum) : (thetaEquiv datum) (minusE datum) = plusD datum

@[simp]

theorem Undecidability.HostYStage.thetaEquiv_minusC (datum : Thue.StandingDatum) : (thetaEquiv datum) (minusC datum) = plusC datum

@[simp]

theorem Undecidability.HostYStage.thetaEquiv_minusT (datum : Thue.StandingDatum) : (thetaEquiv datum) (minusT datum) = plusK datum

@[simp]

theorem Undecidability.HostYStage.thetaEquiv_minusS1 (datum : Thue.StandingDatum) : (thetaEquiv datum) (minusS1 datum) = (plusS2 datum)⁻¹

noncomputable def Undecidability.HostYStage.thetaData (datum : Thue.StandingDatum) : ThetaData datum

The canonical HNN datum for the first compression.

Equations

• Undecidability.HostYStage.thetaData datum = { equiv := Undecidability.HostYStage.thetaEquiv datum, map_d := ⋯, map_e := ⋯, map_c := ⋯, map_t := ⋯, map_s1 := ⋯ }

@[reducible, inline]

abbrev Undecidability.HostYStage.YStage (datum : Thue.StandingDatum) (theta : ThetaData datum) : Type

The proper HNN extension associated to a ThetaData witness.

Equations

• Undecidability.HostYStage.YStage datum theta = HNNExtension (Undecidability.HostYStage.Gamma datum) (Undecidability.HostYStage.HMinus datum) (Undecidability.HostYStage.HPlus datum) theta.equiv

noncomputable def Undecidability.HostYStage.toYStage (datum : Thue.StandingDatum) (theta : ThetaData datum) : Gamma datum →* YStage datum theta

The canonical inclusion Gamma → G_y.

Equations

• Undecidability.HostYStage.toYStage datum theta = HNNExtension.of

noncomputable def Undecidability.HostYStage.yLetter (datum : Thue.StandingDatum) (theta : ThetaData datum) : YStage datum theta

The paper's y; Mathlib's stable letter is y⁻¹.

Equations

• Undecidability.HostYStage.yLetter datum theta = HNNExtension.t⁻¹

theorem Undecidability.HostYStage.toYStage_injective (datum : Thue.StandingDatum) (theta : ThetaData datum) : Function.Injective ⇑(toYStage datum theta)

theorem Undecidability.HostYStage.y_conjugates_d (datum : Thue.StandingDatum) (theta : ThetaData datum) : (yLetter datum theta)⁻¹ * (toYStage datum theta) (d datum) * yLetter datum theta = ((toYStage datum theta) (e datum))⁻¹

theorem Undecidability.HostYStage.y_conjugates_e (datum : Thue.StandingDatum) (theta : ThetaData datum) : (yLetter datum theta)⁻¹ * (toYStage datum theta) (e datum) * yLetter datum theta = (toYStage datum theta) (d datum)

theorem Undecidability.HostYStage.y_conjugates_c (datum : Thue.StandingDatum) (theta : ThetaData datum) : (yLetter datum theta)⁻¹ * (toYStage datum theta) (c datum) * yLetter datum theta = (toYStage datum theta) (c datum)

theorem Undecidability.HostYStage.y_conjugates_t (datum : Thue.StandingDatum) (theta : ThetaData datum) : (yLetter datum theta)⁻¹ * (toYStage datum theta) (t datum) * yLetter datum theta = (toYStage datum theta) (k datum)

theorem Undecidability.HostYStage.y_conjugates_s1 (datum : Thue.StandingDatum) (theta : ThetaData datum) : (yLetter datum theta)⁻¹ * (toYStage datum theta) (s1 datum) * yLetter datum theta = ((toYStage datum theta) (s2 datum))⁻¹