Borisov's Assertion V

This file proves the support statement called Assertion V in Borisov's normal-form argument. A reduced word in the displayed rank-five basis is expanded literally in the two stable letters. Flat Britton normal form then detects every stable-letter color which occurs in that expansion.

Literal color support

theorem Undecidability.BorisovAssertionV.run_color_map (colors : List (Fin 2)) (hne : colors ≠ []) (u : ℤˣ) (lastCoeff : BorisovHNNModel.Base) : List.map MultipleHNNFlat.Syllable.color (BorisovAssertionIV.run colors hne u lastCoeff) = colors

theorem Undecidability.BorisovAssertionV.run_contains_color (colors : List (Fin 2)) (hne : colors ≠ []) (u : ℤˣ) (lastCoeff : BorisovHNNModel.Base) {color : Fin 2} (hcolor : color ∈ colors) : ∃ s ∈ BorisovAssertionIV.run colors hne u lastCoeff, s.color = color

theorem Undecidability.BorisovAssertionV.factorRun_contains_color (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x : BorisovIntersections.Basis × Bool) (lastCoeff : BorisovHNNModel.Base) {color : Fin 2} (hcolor : color ∈ BorisovAssertionIV.factorColors rules x) : ∃ s ∈ BorisovAssertionIV.factorRun rules hne x lastCoeff, s.color = color

theorem Undecidability.BorisovAssertionV.expansionTail_contains_color (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (letters : List (BorisovIntersections.Basis × Bool)) (x : BorisovIntersections.Basis × Bool) (hx : x ∈ letters) {color : Fin 2} (hcolor : color ∈ BorisovAssertionIV.factorColors rules x) : ∃ s ∈ BorisovAssertionIV.expansionTail rules hne letters, s.color = color

theorem Undecidability.BorisovAssertionV.expansionTail_contains_of_usesStable (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (hsupport : ∀ (i : Fin 3), Thue.ContainsBoth (rules i)) (w : FreeGroup BorisovIntersections.Basis) (gamma : Fin 2) (huses : BorisovIntersections.UsesStable w gamma) : ∃ s ∈ BorisovAssertionIV.expansionTail rules hne w.toWord, s.color = gamma

theorem Undecidability.BorisovAssertionV.uExpansion_contains_of_usesStable (datum : Thue.StandingDatum) (w : FreeGroup BorisovIntersections.Basis) (gamma : Fin 2) (huses : BorisovIntersections.UsesStable w gamma) : ∃ s ∈ (BorisovAssertionIV.uExpansion datum w).toList, s.color = gamma

theorem Undecidability.BorisovAssertionV.vExpansion_contains_of_usesStable (datum : Thue.StandingDatum) (w : FreeGroup BorisovIntersections.Basis) (gamma : Fin 2) (huses : BorisovIntersections.UsesStable w gamma) : ∃ s ∈ (BorisovAssertionIV.vExpansion datum w).toList, s.color = gamma

structure Undecidability.BorisovAssertionV.ExpansionWitness : Type

A basis expansion with its evaluation, reducedness, and stable-letter occurrence properties.

• basis : BorisovIntersections.Basis → BorisovIntersections.G0

  The group-valued basis being expanded.

• word : FreeGroup BorisovIntersections.Basis → BorisovAssertionIV.FlatWord

  The flat expansion assigned to each free basis word.

• contains (w : FreeGroup BorisovIntersections.Basis) (gamma : Fin 2) : BorisovIntersections.UsesStable w gamma → ∃ s ∈ (self.word w).toList, s.color = gamma
• eval (w : FreeGroup BorisovIntersections.Basis) : MultipleHNNFlat.eval BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 (self.word w) = BorisovG0HNN.toHNN ((FreeGroup.lift self.basis) w)

def Undecidability.BorisovAssertionV.uWitness (datum : Thue.StandingDatum) : ExpansionWitness

The expansion witness for the left-rule basis.

Equations

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

def Undecidability.BorisovAssertionV.vWitness (datum : Thue.StandingDatum) : ExpansionWitness

The expansion witness for the right-rule basis.

Equations

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

The base subgroup

theorem Undecidability.BorisovAssertionV.toHNN_mem_base_of_mem_DE {x : BorisovIntersections.G0} (hx : x ∈ BorisovIntersections.DE) : BorisovG0HNN.toHNN x ∈ (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0).range

The subgroup J 0

Swapping the two stable letters

noncomputable def Undecidability.BorisovAssertionV.swapHNN : MultipleHNN.Extension BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 →* MultipleHNN.Extension BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0

The endomorphism of the concrete HNN model induced by interchanging the two symmetric stable generators of the presentation.

Equations

• Undecidability.BorisovAssertionV.swapHNN = Undecidability.BorisovG0NormalForm.swappedToHNN.comp Undecidability.BorisovG0HNN.fromHNN

@[simp]

theorem Undecidability.BorisovAssertionV.swapHNN_toHNN (x : BorisovIntersections.G0) : swapHNN (BorisovG0HNN.toHNN x) = BorisovG0NormalForm.swappedToHNN x

@[simp]

theorem Undecidability.BorisovAssertionV.swapHNN_hnnD : swapHNN BorisovG0HNN.hnnD = BorisovG0HNN.hnnD

@[simp]

theorem Undecidability.BorisovAssertionV.swapHNN_hnnE : swapHNN BorisovG0HNN.hnnE = BorisovG0HNN.hnnE

@[simp]

theorem Undecidability.BorisovAssertionV.swapHNN_hnnS1 : swapHNN BorisovG0HNN.hnnS1 = BorisovG0HNN.hnnS2

@[simp]

theorem Undecidability.BorisovAssertionV.swapHNN_hnnS2 : swapHNN BorisovG0HNN.hnnS2 = BorisovG0HNN.hnnS1

theorem Undecidability.BorisovAssertionV.swapHNN_baseEmbedding (g : BorisovHNNModel.Base) : swapHNN ((MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) g) = (MultipleHNN.baseEmbedding BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0) g

def Undecidability.BorisovAssertionV.swapColor : Fin 2 → Fin 2

Exchange the two stable-letter colors.

Equations

• Undecidability.BorisovAssertionV.swapColor 0 = 1
• Undecidability.BorisovAssertionV.swapColor 1 = 0

theorem Undecidability.BorisovAssertionV.swapColor_injective : Function.Injective swapColor

@[simp]

theorem Undecidability.BorisovAssertionV.swapHNN_stableLetter (color : Fin 2) : swapHNN (MultipleHNNFlat.stableLetter BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 color) = MultipleHNNFlat.stableLetter BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 (swapColor color)

def Undecidability.BorisovAssertionV.swapSyllable (s : BorisovAssertionIV.FlatSyllable) : BorisovAssertionIV.FlatSyllable

Exchange the stable-letter color of a syllable while retaining its sign and coefficient.

Equations

• Undecidability.BorisovAssertionV.swapSyllable s = { color := Undecidability.BorisovAssertionV.swapColor s.color, sign := s.sign, coeff := s.coeff }

def Undecidability.BorisovAssertionV.swapFlatWord (w : BorisovAssertionIV.FlatWord) : BorisovAssertionIV.FlatWord

Exchange the two stable-letter colors throughout a flat word.

Equations

• Undecidability.BorisovAssertionV.swapFlatWord w = { head := w.head, toList := List.map Undecidability.BorisovAssertionV.swapSyllable w.toList, chain := ⋯ }

theorem Undecidability.BorisovAssertionV.swapFlatWord_eval (w : BorisovAssertionIV.FlatWord) : MultipleHNNFlat.eval BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 (swapFlatWord w) = swapHNN (MultipleHNNFlat.eval BorisovHNNModel.A0 BorisovHNNModel.B0 BorisovHNNModel.phi0 w)

theorem Undecidability.BorisovAssertionV.swapFlatWord_contains_one_of_contains_zero (w : BorisovAssertionIV.FlatWord) (hzero : ∃ s ∈ w.toList, s.color = 0) : ∃ s ∈ (swapFlatWord w).toList, s.color = 1

The subgroup J 1

Assertion V

theorem Undecidability.BorisovAssertionV.assertionV (datum : Thue.StandingDatum) (hIV : BorisovIntersections.AssertionIV datum) : BorisovIntersections.AssertionV datum hIV

Borisov's Assertion V, for any proof of Assertion IV. The argument is independent of the particular proof object supplied for Assertion IV.

theorem Undecidability.BorisovAssertionV.assertionV_canonical (datum : Thue.StandingDatum) : BorisovIntersections.AssertionV datum ⋯

The canonical unconditional package, using the proved Assertion IV.

Borisov's subgroup-intersection lemma

This file packages Borisov's Assertions IV and V into the four subgroup intersections used in Lemma 3.5 of the paper.

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

Lemma 3.5 of the paper for the canonical first-stage presentation G₀.