ContextNormalForm

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

structure Undecidability.BorisovContextNormalForm.BaseIntersections (datum : Thue.StandingDatum) : Prop

The two base-intersection statements from Lemma 3.5 of the paper, in the iterated-HNN model. They imply the compatibility needed to restrict the c-HNN extension to the cyclic subgroups generated by d and by e.

• u_inf_DE : BorisovCStage.U datum ⊓ BorisovCStage.DE3 = ⊥
• v_inf_DE : BorisovCStage.V datum ⊓ BorisovCStage.DE3 = ⊥

theorem Undecidability.BorisovContextNormalForm.cEquiv_mem_dCyclic_iff (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BaseIntersections datum) (a : ↥(BorisovCStage.U datum)) : ↑a ∈ BorisovCStage.dCyclic ↔ ↑((BorisovCStage.cEquiv datum hfree) a) ∈ BorisovCStage.dCyclic

The attaching equivalence for the c-stage preserves the cyclic subgroup generated by d. This is the compatibility needed for the exact restricted-HNN presentation of ⟨d,c⟩.

theorem Undecidability.BorisovContextNormalForm.CD_eq_generatedWithStable_d (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovCStage.CD datum hfree = HNNLemmas.generatedWithStable BorisovCStage.dCyclic

The subgroup CD = ⟨c,d⟩ is exactly the restricted c-HNN subgroup over the cyclic base ⟨d⟩.

@[reducible, inline]

abbrev Undecidability.BorisovContextNormalForm.DRestricted (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BaseIntersections datum) : Type

The exact restricted-HNN parameter group for CD = ⟨d,c⟩.

Equations

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

noncomputable def Undecidability.BorisovContextNormalForm.dRestrictedEquivCD (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BaseIntersections datum) : DRestricted datum hfree hinter ≃* ↥(BorisovCStage.CD datum hfree)

Exact subgroup-presentation equivalence for CD = ⟨d,c⟩.

Equations

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

@[simp]

theorem Undecidability.BorisovContextNormalForm.dRestrictedEquivCD_of_coe (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BaseIntersections datum) (x : ↥BorisovCStage.dCyclic) : ↑((dRestrictedEquivCD datum hfree hinter) (HNNExtension.of x)) = (BorisovCStage.of3 datum hfree) ↑x

@[simp]

theorem Undecidability.BorisovContextNormalForm.dRestrictedEquivCD_t_coe (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BaseIntersections datum) : ↑((dRestrictedEquivCD datum hfree hinter) HNNExtension.t) = HNNExtension.t

theorem Undecidability.BorisovContextNormalForm.dRestrictedEquivCD_inv_t_coe (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BaseIntersections datum) : ↑((dRestrictedEquivCD datum hfree hinter) HNNExtension.t⁻¹) = BorisovCStage.c datum hfree

theorem Undecidability.BorisovContextNormalForm.exists_leftContext_of_mem_CD (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BaseIntersections datum) {x : BorisovCStage.Gamma2 datum hfree} (hx : x ∈ BorisovCStage.CD datum hfree) : ∃ (L : BorisovCStage.LeftContext datum hfree), BorisovCStage.leftValue datum hfree L = x

Every element of <c,d> has the irreducible left-context form used in Borisov's Lemma 4.

theorem Undecidability.BorisovContextNormalForm.exists_rightContext_of_mem_CE (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BaseIntersections datum) {x : BorisovCStage.Gamma2 datum hfree} (hx : x ∈ BorisovCStage.CE datum hfree) : ∃ (R : BorisovCStage.RightContext datum hfree), BorisovCStage.rightValue datum hfree R = x

Every element of <c,e> has the irreducible right-context form used in Borisov's Lemma 4.