Documentation

LeanPool.SmallUndecidableGroups.Borisov.Assertions.AssertionIVBoundary

The small exponent-separation facts used in Borisov's Assertion IV. They are consequences of the two homomorphisms from the free base <d,e> to Z, and keep the later Britton-pinch proof independent of word syntax.

source
def Undecidability.BorisovPowerArithmetic.dExponent :
BorisovHNNModel.Base →* Multiplicative ℤ

The homomorphism recording the total exponent of d in the free base group.

Equations
Instances For
    source
    def Undecidability.BorisovPowerArithmetic.eExponent :
    BorisovHNNModel.Base →* Multiplicative ℤ

    The homomorphism recording the total exponent of e in the free base group.

    Equations
    Instances For
      source
      @[simp]
      theorem Undecidability.BorisovPowerArithmetic.dExponent_d :
      Multiplicative.toAdd (dExponent BorisovHNNModel.d) = 1
      source
      @[simp]
      theorem Undecidability.BorisovPowerArithmetic.eExponent_e :
      Multiplicative.toAdd (eExponent BorisovHNNModel.e) = 1
      source
      @[reducible, inline]
      abbrev Undecidability.BorisovPowerArithmetic.scaleFour :
      Multiplicative ℤ →* Multiplicative ℤ

      The cyclic-group homomorphism multiplying an exponent by four.

      Equations
      Instances For
        source
        @[simp]
        theorem Undecidability.BorisovPowerArithmetic.eExponent_alpha (x : BorisovHNNModel.Base) :
        Multiplicative.toAdd (eExponent (BorisovHNNModel.alpha x)) = 4 * Multiplicative.toAdd (eExponent x)
        source
        @[simp]
        theorem Undecidability.BorisovPowerArithmetic.dExponent_beta (x : BorisovHNNModel.Base) :
        Multiplicative.toAdd (dExponent (BorisovHNNModel.beta x)) = 4 * Multiplicative.toAdd (dExponent x)
        source
        theorem Undecidability.BorisovPowerArithmetic.e_pow_mem_A0_dvd (n : ℤ) (h : BorisovHNNModel.e ^ n ∈ BorisovHNNModel.A0) :
        4 ∣ n
        source
        theorem Undecidability.BorisovPowerArithmetic.d_pow_mem_B0_dvd (n : ℤ) (h : BorisovHNNModel.d ^ n ∈ BorisovHNNModel.B0) :
        4 ∣ n
        source
        theorem Undecidability.BorisovPowerArithmetic.fin3_succ_sub_eq_zero_of_abs_lt (i j : Fin 3) (hdiv : 4 ∣ ↑↑i + 1 - (↑↑j + 1)) :
        i = j
        source
        theorem Undecidability.BorisovPowerArithmetic.e_rule_difference_mem_A0_imp_eq (i j : Fin 3) (hmem : BorisovHNNModel.e ^ (↑↑i + 1 - (↑↑j + 1)) ∈ BorisovHNNModel.A0) :
        i = j

        Distinct rule exponents 1,2,3 cannot differ by a nonzero multiple of four in the right associated subgroup <d,e⁴>.

        source
        theorem Undecidability.BorisovPowerArithmetic.d_rule_difference_mem_B0_imp_eq (i j : Fin 3) (hmem : BorisovHNNModel.d ^ (↑↑i + 1 - (↑↑j + 1)) ∈ BorisovHNNModel.B0) :
        i = j

        The symmetric exponent-separation fact in <d⁴,e>.

        source
        theorem Undecidability.BorisovPowerArithmetic.e_rule_power_not_mem_A0 (i : Fin 3) :
        BorisovHNNModel.e ^ (↑↑i + 1) ∉ BorisovHNNModel.A0
        source
        theorem Undecidability.BorisovPowerArithmetic.d_rule_power_not_mem_B0 (i : Fin 3) :
        BorisovHNNModel.d ^ (↑↑i + 1) ∉ BorisovHNNModel.B0

        Borisov Assertion IV: the four boundary cases #

        This file formalizes the finite case analysis on page 770 of Borisov's paper. A displayed basis factor is either one of the stable letters or a decorated rule word d^i W_i e^i; its Boolean sign records whether the factor or its inverse occurs. The theorem boundary_pinch_forces_inverse says that a Britton pinch between consecutive factors forces those factors to be formal inverses. Consequently no such boundary pinch occurs in a freely reduced word on the displayed basis.

        source
        def Undecidability.BorisovAssertionIVBoundary.rulePower (i : Fin 3) :
        ℤ

        The nonzero integer exponent i + 1 associated with a rewriting rule.

        Equations
        Instances For
          source
          def Undecidability.BorisovAssertionIVBoundary.ruleFirst (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (i : Fin 3) :
          Fin 2

          The first letter of the indicated nonempty rule word.

          Equations
          Instances For
            source
            def Undecidability.BorisovAssertionIVBoundary.ruleLast (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (i : Fin 3) :
            Fin 2

            The last letter of the indicated nonempty rule word.

            Equations
            Instances For
              source
              def Undecidability.BorisovAssertionIVBoundary.firstStable (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) :
              BorisovIntersections.Basis × Bool → Fin 2

              The first stable letter in the literal expansion of a signed displayed basis factor.

              Equations
              Instances For
                source
                def Undecidability.BorisovAssertionIVBoundary.lastStable (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) :
                BorisovIntersections.Basis × Bool → Fin 2

                The last stable letter in the literal expansion of a signed displayed basis factor.

                Equations
                Instances For
                  source
                  def Undecidability.BorisovAssertionIVBoundary.factorPrefix :
                  BorisovIntersections.Basis × Bool → BorisovHNNModel.Base

                  Base coefficient before the first stable letter of a factor.

                  Equations
                  Instances For
                    source
                    def Undecidability.BorisovAssertionIVBoundary.suffix :
                    BorisovIntersections.Basis × Bool → BorisovHNNModel.Base

                    Base coefficient after the last stable letter of a factor.

                    Equations
                    Instances For
                      source
                      def Undecidability.BorisovAssertionIVBoundary.boundaryCoefficient (x y : BorisovIntersections.Basis × Bool) :
                      BorisovHNNModel.Base

                      The base-group coefficient at the boundary between two expanded basis letters.

                      Equations
                      Instances For
                        source
                        def Undecidability.BorisovAssertionIVBoundary.associatedForSign (positive : Bool) :
                        Subgroup BorisovHNNModel.Base

                        The associated subgroup for a stable letter with the indicated orientation.

                        Equations
                        Instances For
                          source
                          theorem Undecidability.BorisovAssertionIVBoundary.boundary_pinch_forces_same_factor (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x y : BorisovIntersections.Basis × Bool) (hsign : x.2 ≠ y.2) (hstable : lastStable rules hne x = firstStable rules hne y) (hmem : boundaryCoefficient x y ∈ associatedForSign x.2) :
                          x.1 = y.1

                          The four cases in Borisov's proof of Assertion IV. If consecutive signed displayed factors have opposite signs and their touching stable letters form a Britton pinch, their basis indices are equal.

                          source
                          theorem Undecidability.BorisovAssertionIVBoundary.no_boundary_pinch_of_reduced_pair (rules : Fin 3 → List (Fin 2)) (hne : ∀ (i : Fin 3), rules i ≠ []) (x y : BorisovIntersections.Basis × Bool) (hreduced : x.1 = y.1 → x.2 = y.2) (hsign : x.2 ≠ y.2) (hstable : lastStable rules hne x = firstStable rules hne y) :
                          boundaryCoefficient x y ∉ associatedForSign x.2

                          A freely reduced adjacent pair of displayed factors cannot have a Britton pinch across its boundary.