Documentation

LeanPool.SmallUndecidableGroups.Borisov.Model.G0NormalForm

Concrete normal-form consequences for Borisov's G₀ #

This file specializes the iterated-HNN model in GroupUndecidability.Borisov.Model.G0HNN to the presentation maps and positive words used in Borisov's Assertions IV--V.

Swapped HNN model #

source
noncomputable def Undecidability.BorisovG0NormalForm.swappedGenerator :
Fin 4 → BorisovG0HNN.G0HNN

Interpret the four presentation generators in the HNN model after interchanging s₁ and s₂. The defining relations are symmetric in the two stable letters, so this also descends to G₀.

Equations
Instances For
    source
    theorem Undecidability.BorisovG0NormalForm.swapped_relators (r : FreeGroup (Fin 4)) :
    r ∈ BorisovIntersections.presentation.relSet → (FreeGroup.lift swappedGenerator) r = 1
    source
    noncomputable def Undecidability.BorisovG0NormalForm.swappedToHNN :
    BorisovIntersections.G0 →* BorisovG0HNN.G0HNN

    The model interpretation with the two stable generators exchanged.

    Equations
    Instances For
      source
      @[simp]
      theorem Undecidability.BorisovG0NormalForm.swappedToHNN_of (i : Fin 4) :
      swappedToHNN (PresentedGroup.of i) = swappedGenerator i
      source
      @[simp]
      theorem Undecidability.BorisovG0NormalForm.swappedToHNN_stable_one :
      swappedToHNN (BorisovIntersections.stable 1) = BorisovG0HNN.hnnS1

      Positive stable words #

      source
      noncomputable def Undecidability.BorisovG0NormalForm.modelPositive (w : List (Fin 2)) :
      BorisovG0HNN.G0HNN

      Evaluate a positive binary word at the two model stable generators.

      Equations
      Instances For
        source
        @[simp]
        theorem Undecidability.BorisovG0NormalForm.toHNN_positiveWord (w : List (Fin 2)) :
        BorisovG0HNN.toHNN (BorisovIntersections.evalWord (BorisovIntersections.positiveWord w)) = modelPositive w
        source
        theorem Undecidability.BorisovG0NormalForm.count_zero_pos_of_containsBoth {w : List (Fin 2)} (hw : Thue.ContainsBoth w) :
        0 < List.count 0 w

        Images of the displayed A_i and B_i #

        source
        @[simp]
        theorem Undecidability.BorisovG0NormalForm.toHNN_d :
        BorisovG0HNN.toHNN BorisovIntersections.d = BorisovG0HNN.hnnD
        source
        @[simp]
        theorem Undecidability.BorisovG0NormalForm.toHNN_e :
        BorisovG0HNN.toHNN BorisovIntersections.e = BorisovG0HNN.hnnE
        source
        @[simp]
        theorem Undecidability.BorisovG0NormalForm.toHNN_stable_zero :
        BorisovG0HNN.toHNN (BorisovIntersections.stable 0) = BorisovG0HNN.hnnS1
        source
        @[simp]
        theorem Undecidability.BorisovG0NormalForm.toHNN_stable_one :
        BorisovG0HNN.toHNN (BorisovIntersections.stable 1) = BorisovG0HNN.hnnS2
        source
        @[simp]
        theorem Undecidability.BorisovG0NormalForm.toHNN_a (datum : Thue.StandingDatum) (i : Fin 3) :
        BorisovG0HNN.toHNN (BorisovIntersections.a datum i) = BorisovG0HNN.hnnD ^ (↑i + 1) * modelPositive (datum.F i) * BorisovG0HNN.hnnE ^ (↑i + 1)
        source
        @[simp]
        theorem Undecidability.BorisovG0NormalForm.toHNN_b (datum : Thue.StandingDatum) (i : Fin 3) :
        BorisovG0HNN.toHNN (BorisovIntersections.b datum i) = BorisovG0HNN.hnnD ^ (↑i + 1) * modelPositive (datum.E i) * BorisovG0HNN.hnnE ^ (↑i + 1)

        Concrete support exclusions #

        source
        theorem Undecidability.BorisovG0NormalForm.toHNN_mem_stageOne_of_mem_J_zero {x : BorisovIntersections.G0} (hx : x ∈ BorisovIntersections.J 0) :
        BorisovG0HNN.toHNN x ∈ BorisovG0HNN.g1ToG0HNN.range
        source
        theorem Undecidability.BorisovG0NormalForm.swappedToHNN_mem_stageOne_of_mem_J_one {x : BorisovIntersections.G0} (hx : x ∈ BorisovIntersections.J 1) :
        swappedToHNN x ∈ BorisovG0HNN.g1ToG0HNN.range