This file isolates Borisov's c-stage (his group Γ₂) in the actual iterated-HNN model of Γ₃.

Literature: V. V. Borisov, Simple examples of groups with unsolvable word problem (1969), Assertions IV--V and Lemma 4, English translation pp. 769--772. The specialization with exponent α = 4 is checked in M. Tancer, Simpler algorithmically unrecognizable 4-manifolds, Appendix, pp. 26--27.

The construction needs the two displayed rank-five systems to be free. The structure below packages exactly this freeness input.

@[reducible, inline]

abbrev Undecidability.BorisovCStage.RuleBasis : Type

Indices for s₁,s₂,A₁,A₂,A₃ and s₁,s₂,B₁,B₂,B₃.

Equations

• Undecidability.BorisovCStage.RuleBasis = (Fin 2 ⊕ Fin 3)

noncomputable def Undecidability.BorisovCStage.stable3 (beta : Fin 2) : BorisovHNNModel.Gamma3

The stable generator of the two-HNN-extension group with the indicated color.

Equations

• Undecidability.BorisovCStage.stable3 beta = if beta = 0 then Undecidability.BorisovHNNModel.firstStableInStageThree else Undecidability.BorisovHNNModel.secondStableInStageThree

noncomputable def Undecidability.BorisovCStage.positive3 (w : List (Fin 2)) : BorisovHNNModel.Gamma3

Evaluate a positive binary word at the two stable generators.

Equations

• Undecidability.BorisovCStage.positive3 w = Undecidability.Thue.evalPositive Undecidability.BorisovHNNModel.firstStableInStageThree Undecidability.BorisovHNNModel.secondStableInStageThree w

noncomputable def Undecidability.BorisovCStage.a3 (datum : Thue.StandingDatum) (i : Fin 3) : BorisovHNNModel.Gamma3

A_i = d^i F_i e^i, with Lean's i zero-based.

Equations

• Undecidability.BorisovCStage.a3 datum i = Undecidability.BorisovHNNModel.d3 ^ (↑i + 1) * Undecidability.BorisovCStage.positive3 (datum.F i) * Undecidability.BorisovHNNModel.e3 ^ (↑i + 1)

noncomputable def Undecidability.BorisovCStage.b3 (datum : Thue.StandingDatum) (i : Fin 3) : BorisovHNNModel.Gamma3

B_i = d^i E_i e^i, with Lean's i zero-based.

Equations

• Undecidability.BorisovCStage.b3 datum i = Undecidability.BorisovHNNModel.d3 ^ (↑i + 1) * Undecidability.BorisovCStage.positive3 (datum.E i) * Undecidability.BorisovHNNModel.e3 ^ (↑i + 1)

noncomputable def Undecidability.BorisovCStage.uBasis (datum : Thue.StandingDatum) : RuleBasis → BorisovHNNModel.Gamma3

The stable and left-rule generators of the source amalgamating subgroup.

Equations

• Undecidability.BorisovCStage.uBasis datum (Sum.inl beta) = Undecidability.BorisovCStage.stable3 beta
• Undecidability.BorisovCStage.uBasis datum (Sum.inr i) = Undecidability.BorisovCStage.a3 datum i

noncomputable def Undecidability.BorisovCStage.vBasis (datum : Thue.StandingDatum) : RuleBasis → BorisovHNNModel.Gamma3

The stable and right-rule generators of the target amalgamating subgroup.

Equations

• Undecidability.BorisovCStage.vBasis datum (Sum.inl beta) = Undecidability.BorisovCStage.stable3 beta
• Undecidability.BorisovCStage.vBasis datum (Sum.inr i) = Undecidability.BorisovCStage.b3 datum i

noncomputable def Undecidability.BorisovCStage.uLift (datum : Thue.StandingDatum) : FreeGroup RuleBasis →* BorisovHNNModel.Gamma3

The homomorphism freely extending the source amalgamating basis.

Equations

• Undecidability.BorisovCStage.uLift datum = FreeGroup.lift (Undecidability.BorisovCStage.uBasis datum)

noncomputable def Undecidability.BorisovCStage.vLift (datum : Thue.StandingDatum) : FreeGroup RuleBasis →* BorisovHNNModel.Gamma3

The homomorphism freely extending the target amalgamating basis.

Equations

• Undecidability.BorisovCStage.vLift datum = FreeGroup.lift (Undecidability.BorisovCStage.vBasis datum)

structure Undecidability.BorisovCStage.RankFiveFree (datum : Thue.StandingDatum) : Prop

Borisov's Assertion IV in the exact form required to build the c-HNN extension.

• u_injective : Function.Injective ⇑(uLift datum)
• v_injective : Function.Injective ⇑(vLift datum)

@[reducible, inline]

noncomputable abbrev Undecidability.BorisovCStage.U (datum : Thue.StandingDatum) : Subgroup BorisovHNNModel.Gamma3

The subgroup generated by the stable generators and the left rewriting-rule words.

Equations

• Undecidability.BorisovCStage.U datum = (Undecidability.BorisovCStage.uLift datum).range

@[reducible, inline]

noncomputable abbrev Undecidability.BorisovCStage.V (datum : Thue.StandingDatum) : Subgroup BorisovHNNModel.Gamma3

The subgroup generated by the stable generators and the right rewriting-rule words.

Equations

• Undecidability.BorisovCStage.V datum = (Undecidability.BorisovCStage.vLift datum).range

noncomputable def Undecidability.BorisovCStage.cEquiv (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : ↥(U datum) ≃* ↥(V datum)

The letterwise correspondence s_beta ↦ s_beta, A_i ↦ B_i.

Equations

• Undecidability.BorisovCStage.cEquiv datum hfree = Undecidability.HNNLemmas.rangeEquiv (Undecidability.BorisovCStage.uLift datum) (Undecidability.BorisovCStage.vLift datum) ⋯ ⋯

@[simp]

theorem Undecidability.BorisovCStage.cEquiv_on_basis (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (q : RuleBasis) : ↑((cEquiv datum hfree) ⟨uBasis datum q, ⋯⟩) = vBasis datum q

@[reducible, inline]

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

Borisov's Γ₂, with Mathlib's stable letter equal to c⁻¹.

Equations

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

noncomputable def Undecidability.BorisovCStage.of3 (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : BorisovHNNModel.Gamma3 →* Gamma2 datum hfree

The base-group inclusion into the rewriting-rule HNN extension.

Equations

• Undecidability.BorisovCStage.of3 datum hfree = HNNExtension.of

noncomputable def Undecidability.BorisovCStage.c (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : Gamma2 datum hfree

Borisov's generator c; Mathlib's HNN stable letter is c⁻¹.

Equations

• Undecidability.BorisovCStage.c datum hfree = HNNExtension.t⁻¹

theorem Undecidability.BorisovCStage.of3_injective (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : Function.Injective ⇑(of3 datum hfree)

theorem Undecidability.BorisovCStage.c_conjugates_basis (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (q : RuleBasis) : (c datum hfree)⁻¹ * (of3 datum hfree) (uBasis datum q) * c datum hfree = (of3 datum hfree) (vBasis datum q)

The defining c-conjugation law on all five displayed basis elements.

theorem Undecidability.BorisovCStage.c_commutes_stable (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (beta : Fin 2) : Commute ((of3 datum hfree) (stable3 beta)) (c datum hfree)

theorem Undecidability.BorisovCStage.c_simulation (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (i : Fin 3) : (c datum hfree)⁻¹ * (of3 datum hfree) (a3 datum i) * c datum hfree = (of3 datum hfree) (b3 datum i)

The three simulator relations c⁻¹ A_i c = B_i.

The stable-letter projection and the zero-c case of Lemma 4

noncomputable def Undecidability.BorisovCStage.stableProjection1 : BorisovHNNModel.Stage1 →* FreeGroup (Fin 2)

Kill d,e and retain the first HNN stable letter as the first free generator.

Equations

• Undecidability.BorisovCStage.stableProjection1 = HNNExtension.lift 1 (FreeGroup.of 0) Undecidability.BorisovCStage.stableProjection1._proof_1

@[simp]

theorem Undecidability.BorisovCStage.stableProjection1_of0 (x : BorisovHNNModel.Base) : stableProjection1 (BorisovHNNModel.of0 x) = 1

@[simp]

theorem Undecidability.BorisovCStage.stableProjection1_s1 : stableProjection1 BorisovHNNModel.s1 = FreeGroup.of 0

noncomputable def Undecidability.BorisovCStage.stableProjection3 : BorisovHNNModel.Gamma3 →* FreeGroup (Fin 2)

Kill d,e and remember s₁,s₂ as a free basis. This is the projection used in Borisov's m = 0 argument.

Equations

• Undecidability.BorisovCStage.stableProjection3 = HNNExtension.lift Undecidability.BorisovCStage.stableProjection1 (FreeGroup.of 1) Undecidability.BorisovCStage.stableProjection3._proof_2

@[simp]

theorem Undecidability.BorisovCStage.stableProjection3_d : stableProjection3 BorisovHNNModel.d3 = 1

@[simp]

theorem Undecidability.BorisovCStage.stableProjection3_e : stableProjection3 BorisovHNNModel.e3 = 1

@[simp]

theorem Undecidability.BorisovCStage.stableProjection3_s1 : stableProjection3 BorisovHNNModel.firstStableInStageThree = FreeGroup.of 0

@[simp]

theorem Undecidability.BorisovCStage.stableProjection3_s2 : stableProjection3 BorisovHNNModel.secondStableInStageThree = FreeGroup.of 1

def Undecidability.BorisovCStage.positiveFree (w : List (Fin 2)) : FreeGroup (Fin 2)

The positive monoid on two letters, embedded in its free group.

Equations

• Undecidability.BorisovCStage.positiveFree w = FreeGroup.mk (List.map (fun (i : Fin 2) => (i, true)) w)

theorem Undecidability.BorisovCStage.positiveFree_eq_eval (w : List (Fin 2)) : positiveFree w = Thue.evalPositive (FreeGroup.of 0) (FreeGroup.of 1) w

theorem Undecidability.BorisovCStage.stableProjection3_positive (w : List (Fin 2)) : stableProjection3 (positive3 w) = positiveFree w

theorem Undecidability.BorisovCStage.positiveFree_injective : Function.Injective positiveFree

noncomputable def Undecidability.BorisovCStage.DE3 : Subgroup BorisovHNNModel.Gamma3

The base subgroup <d,e> of Γ₃.

Equations

• Undecidability.BorisovCStage.DE3 = Subgroup.closure {Undecidability.BorisovHNNModel.d3, Undecidability.BorisovHNNModel.e3}

theorem Undecidability.BorisovCStage.DE3_le_projection_ker : DE3 ≤ stableProjection3.ker

theorem Undecidability.BorisovCStage.lemma4_zero_c (P Q : List (Fin 2)) (L R : BorisovHNNModel.Gamma3) (hL : L ∈ DE3) (hR : R ∈ DE3) (heq : (positive3 P)⁻¹ * L * positive3 Q * R = 1) : P = Q

Borisov Lemma 4 when the context contains no c: projecting to the free group on s₁,s₂ forces the two positive words to be literally equal.

The exact normal-form statement of Borisov's Lemma 4

noncomputable def Undecidability.BorisovCStage.dCyclic : Subgroup BorisovHNNModel.Gamma3

The cyclic subgroup generated by d in the two-HNN-extension group.

Equations

• Undecidability.BorisovCStage.dCyclic = Subgroup.closure {Undecidability.BorisovHNNModel.d3}

noncomputable def Undecidability.BorisovCStage.eCyclic : Subgroup BorisovHNNModel.Gamma3

The cyclic subgroup generated by e in the two-HNN-extension group.

Equations

• Undecidability.BorisovCStage.eCyclic = Subgroup.closure {Undecidability.BorisovHNNModel.e3}

theorem Undecidability.BorisovCStage.dCyclic_le_DE3 : dCyclic ≤ DE3

theorem Undecidability.BorisovCStage.eCyclic_le_DE3 : eCyclic ≤ DE3

@[reducible, inline]

abbrev Undecidability.BorisovCStage.CReducedWord (datum : Thue.StandingDatum) (_hfree : RankFiveFree datum) : Type

Reduced normal words in the rewriting-rule HNN extension.

Equations

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

structure Undecidability.BorisovCStage.LeftContext (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : Type

An HNN-reduced word on {c,d}. Its base coefficients are all powers of d; its stable-letter list is the list of occurrences of c^{±1}.

• word : CReducedWord datum hfree

  The reduced normal word of the left context.

• head_mem : self.word.head ∈ dCyclic
• coeff_mem (p : ℤˣ × BorisovHNNModel.Gamma3) : p ∈ self.word.toList → p.2 ∈ dCyclic

structure Undecidability.BorisovCStage.RightContext (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : Type

An HNN-reduced word on {c,e}.

• word : CReducedWord datum hfree

  The reduced normal word of the right context.

• head_mem : self.word.head ∈ eCyclic
• coeff_mem (p : ℤˣ × BorisovHNNModel.Gamma3) : p ∈ self.word.toList → p.2 ∈ eCyclic

noncomputable def Undecidability.BorisovCStage.leftValue (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (L : LeftContext datum hfree) : Gamma2 datum hfree

The group element represented by a left context.

Equations

• Undecidability.BorisovCStage.leftValue datum hfree L = HNNExtension.NormalWord.ReducedWord.prod (Undecidability.BorisovCStage.cEquiv datum hfree) L.word

noncomputable def Undecidability.BorisovCStage.rightValue (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (R : RightContext datum hfree) : Gamma2 datum hfree

The group element represented by a right context.

Equations

• Undecidability.BorisovCStage.rightValue datum hfree R = HNNExtension.NormalWord.ReducedWord.prod (Undecidability.BorisovCStage.cEquiv datum hfree) R.word

noncomputable def Undecidability.BorisovCStage.positive2 (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (w : List (Fin 2)) : Gamma2 datum hfree

Evaluate a positive stable-letter word after adjoining the rule-transport generator.

Equations

• Undecidability.BorisovCStage.positive2 datum hfree w = (Undecidability.BorisovCStage.of3 datum hfree) (Undecidability.BorisovCStage.positive3 w)

def Undecidability.BorisovCStage.Lemma4Equation (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (P Q : List (Fin 2)) (L : LeftContext datum hfree) (R : RightContext datum hfree) : Prop

The published hypothesis P⁻¹ L Q R = 1, with L and R already in the irreducible forms used in Borisov's induction.

Equations

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

def Undecidability.BorisovCStage.BorisovLemma4 (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : Prop

Exact c-stage separation theorem needed by the converse direction.

This is Borisov 1969, Lemma 4, specialized to N = 2, M = 3, α = 4. The induction measure in the paper is the number of positive occurrences of c in L.word.toList ++ R.word.toList (equivalently one half of its length).

Equations

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

theorem Undecidability.BorisovCStage.lemma4_of_context_lists_nil (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (P Q : List (Fin 2)) (L : LeftContext datum hfree) (R : RightContext datum hfree) (hLnil : L.word.toList = []) (hRnil : R.word.toList = []) (heq : Lemma4Equation datum hfree P Q L R) : ThueEq (Thue.systemOf datum.F datum.E) Q P

The m = 0 branch of the published induction in the iterated HNN model.

Context subgroups and factorization

noncomputable def Undecidability.BorisovCStage.CD (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : Subgroup (Gamma2 datum hfree)

The subgroup generated by the rule-transport generator and d.

Equations

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

noncomputable def Undecidability.BorisovCStage.CE (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : Subgroup (Gamma2 datum hfree)

The subgroup generated by the rule-transport generator and e.

Equations

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

theorem Undecidability.BorisovCStage.equation_iff_factorization {G : Type u_1} [Group G] (P L Q R : G) : P⁻¹ * L * Q * R = 1 ↔ P = L * Q * R

Isolating the positive-c induction step

theorem Undecidability.BorisovCStage.thueStep_rule_forward (datum : Thue.StandingDatum) (l r : List (Fin 2)) (i : Fin 3) : ThueStep (Thue.systemOf datum.F datum.E) (l ++ datum.F i ++ r) (l ++ datum.E i ++ r)

theorem Undecidability.BorisovCStage.thueStep_rule_backward (datum : Thue.StandingDatum) (l r : List (Fin 2)) (i : Fin 3) : ThueStep (Thue.systemOf datum.F datum.E) (l ++ datum.E i ++ r) (l ++ datum.F i ++ r)

def Undecidability.BorisovCStage.contextComplexity (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (L : LeftContext datum hfree) (R : RightContext datum hfree) : ℕ

The total stable-letter length of the two surrounding contexts.

Equations

• Undecidability.BorisovCStage.contextComplexity datum hfree L R = L.word.toList.length + R.word.toList.length

def Undecidability.BorisovCStage.PinchReduction (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : Prop

The key deep local statement in Borisov's Lemma 4.

If the context is nonempty, Britton reduction plus Assertions IV--V must exhibit one semigroup rule in Q and new irreducible contexts with strictly fewer occurrences of c^{±1}. Tancer's Appendix carries out precisely this case analysis for α = 4.

Equations

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

theorem Undecidability.BorisovCStage.borisovLemma4_of_pinchReduction (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) (hpinch : PinchReduction datum hfree) : BorisovLemma4 datum hfree

Once the local pinch-reduction statement is available, well-founded induction gives all of Borisov's Lemma 4.

Exponent balance (Borisov's use of Lemma 3)

noncomputable def Undecidability.BorisovCStage.cExponent (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : Gamma2 datum hfree →* Multiplicative ℤ

Exponent sum of Mathlib's stable letter t = c⁻¹.

Equations

• Undecidability.BorisovCStage.cExponent datum hfree = HNNExtension.lift 1 (Multiplicative.ofAdd 1) ⋯

@[simp]

theorem Undecidability.BorisovCStage.cExponent_c (datum : Thue.StandingDatum) (hfree : RankFiveFree datum) : (cExponent datum hfree) (c datum hfree) = Multiplicative.ofAdd (-1)