ConverseCore

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

theorem Undecidability.BorisovDoubleCosetBridge.lastTwoStages_force_doubleCoset {G : Type u_1} [Group G] (A C : Subgroup G) (P Q : G) (hcomm : Commute ((HNNLemmas.centralizerOf (HNNLemmas.generatedWith (Subgroup.map (HNNLemmas.centralizerOf C) A) (HNNLemmas.conjugatedStable C P))) (HNNLemmas.conjugatedStable C Q)) (HNNLemmas.centralizerStable (HNNLemmas.generatedWith (Subgroup.map (HNNLemmas.centralizerOf C) A) (HNNLemmas.conjugatedStable C P)))) : ∃ (c : ↥C) (a : ↥A), P = ↑c * Q * ↑a

Sharp form of the last two HNN reductions in Borisov's converse.

The last stable letter k centralizes the subgroup generated by the image of A and P⁻¹tP. If Q⁻¹tQ commutes with k, comparison of the first stable-letter coefficient gives the ordered double-coset equation P = c * Q * a, with c ∈ C and a ∈ A.

theorem Undecidability.BorisovDoubleCosetBridge.lastTwoStages_force_doubleCoset_of_commutator {G : Type u_1} [Group G] (A C : Subgroup G) (P Q : G) (hcommutator : ((HNNLemmas.centralizerOf (HNNLemmas.generatedWith (Subgroup.map (HNNLemmas.centralizerOf C) A) (HNNLemmas.conjugatedStable C P))) (HNNLemmas.conjugatedStable C Q))⁻¹ * (HNNLemmas.centralizerStable (HNNLemmas.generatedWith (Subgroup.map (HNNLemmas.centralizerOf C) A) (HNNLemmas.conjugatedStable C P)))⁻¹ * (HNNLemmas.centralizerOf (HNNLemmas.generatedWith (Subgroup.map (HNNLemmas.centralizerOf C) A) (HNNLemmas.conjugatedStable C P))) (HNNLemmas.conjugatedStable C Q) * HNNLemmas.centralizerStable (HNNLemmas.generatedWith (Subgroup.map (HNNLemmas.centralizerOf C) A) (HNNLemmas.conjugatedStable C P)) = 1) : ∃ (c : ↥C) (a : ↥A), P = ↑c * Q * ↑a

The same result for the commutator convention used by Borisov.testWord.

@[reducible, inline]

abbrev Undecidability.BorisovConverseCore.TStage (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Type

The t-stage of Borisov's model, with t centralizing <c,d>.

Equations

• Undecidability.BorisovConverseCore.TStage datum hfree = Undecidability.HNNLemmas.CentralizerHNN (Undecidability.BorisovCStage.Gamma2 datum hfree) (Undecidability.BorisovCStage.CD datum hfree)

noncomputable def Undecidability.BorisovConverseCore.toTStage (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : BorisovCStage.Gamma2 datum hfree →* TStage datum hfree

The inclusion into the HNN extension adjoining the generator t.

Equations

• Undecidability.BorisovConverseCore.toTStage datum hfree = Undecidability.HNNLemmas.centralizerOf (Undecidability.BorisovCStage.CD datum hfree)

noncomputable def Undecidability.BorisovConverseCore.tLetter (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : TStage datum hfree

The new stable letter t in its centralizer HNN extension.

Equations

• Undecidability.BorisovConverseCore.tLetter datum hfree = Undecidability.HNNLemmas.centralizerStable (Undecidability.BorisovCStage.CD datum hfree)

noncomputable def Undecidability.BorisovConverseCore.conjugatedT (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (w : List (Fin 2)) : TStage datum hfree

The conjugate of t by the evaluated positive binary word.

Equations

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

noncomputable def Undecidability.BorisovConverseCore.KSubgroup (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Subgroup (TStage datum hfree)

The subgroup centralized by Borisov's final letter k.

Equations

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

@[reducible, inline]

abbrev Undecidability.BorisovConverseCore.FinalStage (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : Type

The final k-stage of the semantic HNN model.

Equations

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

noncomputable def Undecidability.BorisovConverseCore.toFinalStage (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) : TStage datum hfree →* FinalStage datum hfree

The inclusion into the final HNN extension adjoining the generator k.

Equations

• Undecidability.BorisovConverseCore.toFinalStage datum hfree = Undecidability.HNNLemmas.centralizerOf (Undecidability.BorisovConverseCore.KSubgroup datum hfree)

noncomputable def Undecidability.BorisovConverseCore.finalConjugatedT (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (w : List (Fin 2)) : FinalStage datum hfree

The conjugated test element carried into the final HNN extension.

Equations

• Undecidability.BorisovConverseCore.finalConjugatedT datum hfree w = (Undecidability.BorisovConverseCore.toFinalStage datum hfree) (Undecidability.BorisovConverseCore.conjugatedT datum hfree w)

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

The final stable letter k.

Equations

• Undecidability.BorisovConverseCore.kLetter datum hfree = Undecidability.HNNLemmas.centralizerStable (Undecidability.BorisovConverseCore.KSubgroup datum hfree)

theorem Undecidability.BorisovConverseCore.thueEq_of_context_factorization (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BorisovContextNormalForm.BaseIntersections datum) (hlemma4 : BorisovCStage.BorisovLemma4 datum hfree) (Q : List (Fin 2)) (hfactor : ∃ (l : ↥(BorisovCStage.CD datum hfree)) (r : ↥(BorisovCStage.CE datum hfree)), BorisovCStage.positive2 datum hfree datum.P = ↑l * BorisovCStage.positive2 datum hfree Q * ↑r) : ThueEq (Thue.systemOf datum.F datum.E) Q datum.P

Ordered double-coset factorization in the c-stage produces the exact irreducible equation consumed by Borisov's Lemma 4.

theorem Undecidability.BorisovConverseCore.model_test_eq_one_imp_thueEq (datum : Thue.StandingDatum) (hfree : BorisovCStage.RankFiveFree datum) (hinter : BorisovContextNormalForm.BaseIntersections datum) (hlemma4 : BorisovCStage.BorisovLemma4 datum hfree) (Q : List (Fin 2)) (htest : (finalConjugatedT datum hfree Q)⁻¹ * (kLetter datum hfree)⁻¹ * finalConjugatedT datum hfree Q * kLetter datum hfree = 1) : ThueEq (Thue.systemOf datum.F datum.E) Q datum.P

Fully formal last-two-stage implication. Once Assertions IV--V provide the base intersections and the local Lemma-4 induction, triviality of the test commutator in the semantic HNN model implies the desired Thue equality.