This file derives the canonical reduced-word consequences of Borisov's Assertions IV--V and proves the four subgroup intersections in Lemma 3.5 of the paper.

The normal-form input is stated for canonical reduced words in the displayed free bases. A rule-basis letter is declared to use both stable letters; this is exactly where StandingDatum.F_support and StandingDatum.E_support enter the paper proof. Assertion V, followed by comparison of multiple-HNN normal forms, says that a basis word representing an element of J beta cannot use the other stable letter, and one representing an element of <d,e> cannot use either stable letter.

@[reducible, inline]

abbrev Undecidability.BorisovIntersections.G0Word : Type

Words on the four generators d, e, s₁, s₂ of the initial Borisov stage.

Equations

• Undecidability.BorisovIntersections.G0Word = Undecidability.Word 4

def Undecidability.BorisovIntersections.dWord : G0Word

Generator order at the first Borisov stage: d,e,s1,s2.

Equations

• Undecidability.BorisovIntersections.dWord = Undecidability.Word.generator 0

def Undecidability.BorisovIntersections.eWord : G0Word

The one-letter word representing e.

Equations

• Undecidability.BorisovIntersections.eWord = Undecidability.Word.generator 1

def Undecidability.BorisovIntersections.s1Word : G0Word

The one-letter word representing the first stable generator.

Equations

• Undecidability.BorisovIntersections.s1Word = Undecidability.Word.generator 2

def Undecidability.BorisovIntersections.s2Word : G0Word

The one-letter word representing the second stable generator.

Equations

• Undecidability.BorisovIntersections.s2Word = Undecidability.Word.generator 3

def Undecidability.BorisovIntersections.stableWord (beta : Fin 2) : G0Word

The word representing the stable generator with the selected color.

Equations

• Undecidability.BorisovIntersections.stableWord beta = if beta = 0 then Undecidability.BorisovIntersections.s1Word else Undecidability.BorisovIntersections.s2Word

def Undecidability.BorisovIntersections.positiveWord (w : List (Fin 2)) : G0Word

Substitute the two stable-generator words into a positive binary word.

Equations

• Undecidability.BorisovIntersections.positiveWord w = Undecidability.Word.substitutePositive Undecidability.BorisovIntersections.s1Word Undecidability.BorisovIntersections.s2Word w

def Undecidability.BorisovIntersections.sDRelator (s : G0Word) : G0Word

The relator imposing s⁻¹ * d⁴ * s = d.

Equations

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

def Undecidability.BorisovIntersections.sERelator (s : G0Word) : G0Word

The relator imposing s⁻¹ * e * s = e⁴.

Equations

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

def Undecidability.BorisovIntersections.presentation : FP 4 4

The four-generator, four-relator first stage G0, corresponding to Γ₁ in equation (1) of the paper.

Equations

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

@[reducible, inline]

abbrev Undecidability.BorisovIntersections.G0 : Type

The group defined by the initial four-relator Borisov presentation.

Equations

• Undecidability.BorisovIntersections.G0 = Undecidability.BorisovIntersections.presentation.Group

def Undecidability.BorisovIntersections.evalWord (w : G0Word) : G0

Evaluate a four-generator word in the initial Borisov presented group.

Equations

• Undecidability.BorisovIntersections.evalWord w = Undecidability.BorisovIntersections.presentation.evalWord w

def Undecidability.BorisovIntersections.d : G0

The generator d in the initial presented group.

Equations

• Undecidability.BorisovIntersections.d = Undecidability.BorisovIntersections.evalWord Undecidability.BorisovIntersections.dWord

def Undecidability.BorisovIntersections.e : G0

The generator e in the initial presented group.

Equations

• Undecidability.BorisovIntersections.e = Undecidability.BorisovIntersections.evalWord Undecidability.BorisovIntersections.eWord

def Undecidability.BorisovIntersections.stable (beta : Fin 2) : G0

The stable generator with the indicated color in the initial presented group.

Equations

• Undecidability.BorisovIntersections.stable beta = Undecidability.BorisovIntersections.evalWord (Undecidability.BorisovIntersections.stableWord beta)

def Undecidability.BorisovIntersections.aWord (datum : Thue.StandingDatum) (i : Fin 3) : G0Word

A_i = d^i F_i e^i, with Lean's index i starting at zero.

Equations

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

def Undecidability.BorisovIntersections.bWord (datum : Thue.StandingDatum) (i : Fin 3) : G0Word

B_i = d^i E_i e^i, with Lean's index i starting at zero.

Equations

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

def Undecidability.BorisovIntersections.a (datum : Thue.StandingDatum) (i : Fin 3) : G0

The evaluated left rewriting-rule word in the initial presented group.

Equations

• Undecidability.BorisovIntersections.a datum i = Undecidability.BorisovIntersections.evalWord (Undecidability.BorisovIntersections.aWord datum i)

def Undecidability.BorisovIntersections.b (datum : Thue.StandingDatum) (i : Fin 3) : G0

The evaluated right rewriting-rule word in the initial presented group.

Equations

• Undecidability.BorisovIntersections.b datum i = Undecidability.BorisovIntersections.evalWord (Undecidability.BorisovIntersections.bWord datum i)

@[reducible, inline]

abbrev Undecidability.BorisovIntersections.Basis : Type

Indices for the displayed bases s1,s2,A1,A2,A3 and s1,s2,B1,B2,B3.

Equations

• Undecidability.BorisovIntersections.Basis = (Fin 2 ⊕ Fin 3)

def Undecidability.BorisovIntersections.uBasis (datum : Thue.StandingDatum) : Basis → G0

The two stable generators and three left rewriting-rule generators.

Equations

• Undecidability.BorisovIntersections.uBasis datum (Sum.inl beta) = Undecidability.BorisovIntersections.stable beta
• Undecidability.BorisovIntersections.uBasis datum (Sum.inr i) = Undecidability.BorisovIntersections.a datum i

def Undecidability.BorisovIntersections.vBasis (datum : Thue.StandingDatum) : Basis → G0

The two stable generators and three right rewriting-rule generators.

Equations

• Undecidability.BorisovIntersections.vBasis datum (Sum.inl beta) = Undecidability.BorisovIntersections.stable beta
• Undecidability.BorisovIntersections.vBasis datum (Sum.inr i) = Undecidability.BorisovIntersections.b datum i

def Undecidability.BorisovIntersections.DE : Subgroup G0

The base subgroup <d,e>.

Equations

• Undecidability.BorisovIntersections.DE = Subgroup.closure {Undecidability.BorisovIntersections.d, Undecidability.BorisovIntersections.e}

def Undecidability.BorisovIntersections.J (beta : Fin 2) : Subgroup G0

J_beta = <d,e,s_beta>.

Equations

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

def Undecidability.BorisovIntersections.stableCyclic (beta : Fin 2) : Subgroup G0

The cyclic subgroup generated by the selected stable generator.

Equations

• Undecidability.BorisovIntersections.stableCyclic beta = Subgroup.closure {Undecidability.BorisovIntersections.stable beta}

def Undecidability.BorisovIntersections.Uc (datum : Thue.StandingDatum) : Subgroup G0

U_c = <s1,s2,A1,A2,A3>.

Equations

• Undecidability.BorisovIntersections.Uc datum = Subgroup.closure (Set.range (Undecidability.BorisovIntersections.uBasis datum))

def Undecidability.BorisovIntersections.Vc (datum : Thue.StandingDatum) : Subgroup G0

V_c = <s1,s2,B1,B2,B3>.

Equations

• Undecidability.BorisovIntersections.Vc datum = Subgroup.closure (Set.range (Undecidability.BorisovIntersections.vBasis datum))

theorem Undecidability.BorisovIntersections.uBasis_mem_Uc (datum : Thue.StandingDatum) (q : Basis) : uBasis datum q ∈ Uc datum

theorem Undecidability.BorisovIntersections.vBasis_mem_Vc (datum : Thue.StandingDatum) (q : Basis) : vBasis datum q ∈ Vc datum

theorem Undecidability.BorisovIntersections.stable_mem_J (beta : Fin 2) : stable beta ∈ J beta

structure Undecidability.BorisovIntersections.AssertionIV (datum : Thue.StandingDatum) : Prop

Formal content of Borisov's Assertion IV used by the paper: both displayed generating lists are free bases, and the letterwise correspondence extends to the stated subgroup isomorphism.

• u_free : Function.Injective ⇑(FreeGroup.lift (uBasis datum))
• v_free : Function.Injective ⇑(FreeGroup.lift (vBasis datum))
• correspondence : ∃ (equiv : ↥(Uc datum) ≃* ↥(Vc datum)), ∀ (q : Basis), ↑(equiv ⟨uBasis datum q, ⋯⟩) = vBasis datum q

def Undecidability.BorisovIntersections.UsesStable (w : FreeGroup Basis) (gamma : Fin 2) : Prop

A basis factor literally uses a stable letter. A stable basis factor uses its own index; an A_i or B_i factor uses both indices because every F_i and E_i contains both letters.

Equations

• Undecidability.BorisovIntersections.UsesStable w gamma = ∃ letter ∈ w.toWord, match letter.1 with | Sum.inl beta => beta = gamma | Sum.inr val => True

structure Undecidability.BorisovIntersections.AssertionV (datum : Thue.StandingDatum) (_hIV : AssertionIV datum) : Prop

The exact normal-form consequence of Assertion V needed in Lemma 3.5 of the paper.

Assertion IV makes w.toWord a minimal displayed-basis representative. Assertion V removes every Britton pinch from its literal expansion. Comparing the resulting multiple-HNN normal form with a representative in J beta or in <d,e> gives these four support exclusions.

• u_mem_J (w : FreeGroup Basis) (beta gamma : Fin 2) : (FreeGroup.lift (uBasis datum)) w ∈ J beta → gamma ≠ beta → ¬UsesStable w gamma
• v_mem_J (w : FreeGroup Basis) (beta gamma : Fin 2) : (FreeGroup.lift (vBasis datum)) w ∈ J beta → gamma ≠ beta → ¬UsesStable w gamma
• u_mem_DE (w : FreeGroup Basis) : (FreeGroup.lift (uBasis datum)) w ∈ DE → ∀ (gamma : Fin 2), ¬UsesStable w gamma
• v_mem_DE (w : FreeGroup Basis) : (FreeGroup.lift (vBasis datum)) w ∈ DE → ∀ (gamma : Fin 2), ¬UsesStable w gamma

def Undecidability.BorisovIntersections.other (beta : Fin 2) : Fin 2

Exchange the two stable-generator indices.

Equations

• Undecidability.BorisovIntersections.other beta = if beta = 0 then 1 else 0

theorem Undecidability.BorisovIntersections.Uc_inf_J (datum : Thue.StandingDatum) (beta : Fin 2) (hIV : AssertionIV datum) (hV : AssertionV datum hIV) : Uc datum ⊓ J beta = stableCyclic beta

First half of Lemma 3.5 of the paper: U_c ∩ J_beta = <s_beta>.

theorem Undecidability.BorisovIntersections.Vc_inf_J (datum : Thue.StandingDatum) (beta : Fin 2) (hIV : AssertionIV datum) (hV : AssertionV datum hIV) : Vc datum ⊓ J beta = stableCyclic beta

First half of Lemma 3.5 of the paper: V_c ∩ J_beta = <s_beta>.

theorem Undecidability.BorisovIntersections.Uc_inf_DE (datum : Thue.StandingDatum) (hIV : AssertionIV datum) (hV : AssertionV datum hIV) : Uc datum ⊓ DE = ⊥

Second half of Lemma 3.5 of the paper: U_c ∩ <d,e> = 1.

theorem Undecidability.BorisovIntersections.Vc_inf_DE (datum : Thue.StandingDatum) (hIV : AssertionIV datum) (hV : AssertionV datum hIV) : Vc datum ⊓ DE = ⊥

Second half of Lemma 3.5 of the paper: V_c ∩ <d,e> = 1.

theorem Undecidability.BorisovIntersections.lemma4_2 (datum : Thue.StandingDatum) (hIV : AssertionIV datum) (hV : AssertionV datum hIV) : (∀ (beta : Fin 2), Uc datum ⊓ J beta = stableCyclic beta ∧ Vc datum ⊓ J beta = stableCyclic beta) ∧ Uc datum ⊓ DE = ⊥ ∧ Vc datum ⊓ DE = ⊥

The four intersections in Lemma 3.5 of the paper, bundled together.