Internal repetition for length functions

We formalize (in code) the combinatorial group theory part of the spltting lemma of the paper Homogenous length functions on Groups. This is based on an implementation (in scala) of a large part of Homotopy type theory equipped with symbolic algebra in this project.

The statement

Assume we are given the following:

Then we have the following:

Theorem: There exists a constant $A\in\mathbb{Q}$ so that for $n \in \mathbb{N}$,

$$l(x^{2n}) \leq n(l(y) + l(z)) +A.$$

In the above paper, homogeneity is used to deduce a bound for $l(x)$, and on taking the limit we get $l(x) \leq \frac{l(y) + l(z)}{2}$.

Preliminaries

We start with some imports. This is a bit ugly due to avoiding variable name collisions.

import provingground._, HoTT._

import scalahott._, andrewscurtis.FreeGroups._
import spire.implicits._
import NatRing.{ x=>_,  Literal => nat, leq => natLeq, _}, QField.{w => _, x =>_, y=>_, z=>_, Literal => rat, _}, FreeGroup.{Literal => elem, _}
import Theorems.{PowerDistributive, ConjPower}

The Setup

We introduce terms for the length function $l$, as well as witnesses for the assumptions on $l$.

val l = "l" :: FreeGroup ->: QTyp

val g = "g" :: FreeGroup
val h = "h" :: FreeGroup
val n = "n" :: NatTyp
val triang =
  "triangle-inequality" :: (
    g ~>: (h ~>: (
      (leq(l(g |+| h))(l(g) + l(h)))
    ))
  )
val conjInv =
  "conjugacy-invariance" :: (
    g ~>: (
      h ~>: (
        (l(h) =:= (l(g |+| h |+| g.inverse)))
      )
    )
  )

Next, we introduce variables for $x, y, z, s, t \in G$, where $s, t \in G$ are the elements so that the conjugacies $x \sim wy$ and $x \sim zw^{-1}$ are given by the equations $x = swys^{-1}$ and $x = tzw^{-1}t^{-1}$.

val w = "w" :: FreeGroup
val y = "y" :: FreeGroup
val z = "z" :: FreeGroup
val s = "s" :: FreeGroup
val t = "t" :: FreeGroup

So far these are all independent. We shall introduce terms as witnesses for the above equations later, as we first prove a lemma not involving $x$.

Statement of lemma

The main internal repetition trick is captured the bound

$$l((wy)^ns^{-1}t(zw^{-1})^n)\leq n(l(y) + l(z)) + l(s^{-1}) + l(t).$$

We define $c(n) = (wy)^ns^{-1}t(zw^{-1})^n$ and $f(n) = n(l(y) + l(z)) + l(s^{-1}) + l(t)$, so the inequality is $l(c(n))\leq(f(n))$. We encode this below as the main lemma.

val wy = w |+| y
val zwbar = z |+| w.inverse
val wyn = FreeGroup.power(wy)(n)
val zwbarn = FreeGroup.power(zwbar)(n)
val c = n :-> (wyn |+| s.inverse |+| t |+| zwbarn) // this is the function we have to bound.

val r = incl(QField)

val f = n :-> (l(s.inverse) + l(t) + ((l(y) + l(z)) * r(n) ) )
val lemma = n :-> (leq (l(c(n)) )(f(n) ) )

Proving the lemma

Let $d(n) = (wy)(wy)^ns^{-1}t(zw^{-1})^n(zw)$. Note that by definition $g^{n+1} = g^n g$, so we need to prove $d(n) = c(n+1)$. We use $g^ng^m = g^{n+m}$ (proved in our code) to prove this. The proof is given by the term dIsc.

val d = n :-> (wy |+| wyn |+| s.inverse |+| t |+| zwbarn  |+| zwbar)
val dIsc = FreeGroup.rm(s.inverse |+| t |+| zwbarn |+| zwbar) **: (PowerDistributive.pf(wy)(nat(1))(n))
assert(dIsc.typ == (d(n) =:= c(succ(n))))

Next, let $b(n) = y(wy)^ns^{-1}t(zw^{-1})^nz$ be the conjugacy-reduced form of $d(n)$. Using $d(n) = c(n+1)$ and conjugacy invariance, we show that $l(c(n+1)) = l(b(n))$. The term bIsc is the proof of l(c(n+1)) = l(b(n)).

val b = n :-> (y |+| wyn |+| s.inverse |+| t |+| zwbarn  |+| z)
val lbIsld = conjInv(w)(y |+| c(n) |+| z)
val bIsc = lbIsld && (l **: dIsc)
assert(bIsc.typ == (l(b(n)) =:= l(c(succ(n))) ))

With these preliminaries, we can prove the lemma by induction. First note the base case.

val baseCase = triang(inv(s))(t) !: (lemma(0))

The induction step takes more work. We first assume the induction hypothesis.

val hyp = "hyp" :: lemma(n)

Next, we bound $l(b(n))$ (which we know is $l(c(n+ 1)))$ in terms of $l(c(n))$.

val lbnBoundedlcnlylz = triang(y)(c(n)) + triang(y |+| c(n))(z)
assert(lbnBoundedlcnlylz.typ == (leq(l(b(n)))(l(c(n)) + l(y) + l(z))))

Now, using the induction hypothesis, we get a bound on $l(b(n))$.

val lbnBounded = lbnBoundedlcnlylz + hyp
assert(lbnBounded.typ == leq(l(b(n)) )(f(succ(n))) )

Next, we put together $l(c(n+1)) = l(b(n))$ and the bound on $l(b(n))$ to get the required bound on $l(c(n+1))$.

val bnd = "bound" :: QField.LocalTyp
val cbnd = bIsc.liftWit(bnd :-> (leq(bnd)(f(succ(n)) ) ))
val step = cbnd(lbnBounded)
assert(step.typ == lemma(succ(n)))

Finally, the lemma is proved by induction.

val lemmaProof = Induc(lemma, baseCase, n :~> (hyp :-> step))
assert(lemmaProof.typ == (n ~>: (lemma(n))) )

Rest of the proof of the theorem

Some work remains, essentially to use symbolic algebra for equations such as $x^{2n} = x^nx^n$ and to put together equations and inequalities. We introduce terms witnessing the hypotheses $x=swys^{-1}$ and $x=tzw^{-1}t^{-1}$

val x = "x" :: FreeGroup
// val g = "g" :: FreeGroup
val pown = g :-> FreeGroup.power(g)(n)
val c1 = "x ~ wy" :: (x =:= (s |+| w |+| y |+| s.inverse))
val c2 = "x ~ zw^{-1}" :: (x =:= (t |+| z |+| w.inverse |+| t.inverse))

We deduce using a theorem (in our code) about powers of conjugates that $x^n = s(wy)^ns^{-1} = t(zw^{-1})^nt^{-1}$.

val xnConjwyn = (pown **: c1) && ConjPower.pf(s)(wy)(n)
val xnConjzwbarn= (pown **: c2) && ConjPower.pf(t)(zwbar)(n)
assert(xnConjwyn.typ == (pown(x) =:= (s |+| pown(wy)  |+| s.inverse  ) ) )
assert(xnConjzwbarn.typ == (pown(x) =:= (t |+| pown(zwbar)  |+| t.inverse  ) ) )

We use the above equations to show that $x^nx^n = s(wy)^ns^{-1}t(zw^{-1})^nt^{-1}$.

val t1 = s |+| pown(wy)  |+| s.inverse
val t2 = t |+| pown(zwbar)  |+| t.inverse
val xnxnExpr = (FreeGroup.rm(pown(x)) **: xnConjwyn) && (FreeGroup.lm(t1) **: xnConjzwbarn)
assert(xnxnExpr.typ == ((pown(x) |+| pown(x)) =:= (t1 |+| t2 )   ))

Using $x^nx^n = x^{2n}$, we get the formula $x^{2n} = s(wy)^ns^{-1}t(zw^{-1})^nt^{-1}$.

val x2nExpr =PowerDistributive.pf(x)(n)(n) .symWit && xnxnExpr
assert(x2nExpr.typ == (FreeGroup.power(x)(NatRing.prod(n)(nat(2))) =:= (s |+| c(n) |+| t.inverse)))

We now bound the length of the right hand side $s(wy)^ns^{-1}t(zw^{-1})^nt^{-1}$.

val thmBound = f(n) + l(s) + l(t.inverse)
val exprBound = lemmaProof(n) + triang(s)(c(n)) + triang(s |+| c(n))(t.inverse)
assert(exprBound.typ == leq(l(s |+| c(n) |+| t.inverse ))(thmBound))

We easily deduce the bound on $l(x^{2n})$ to complete the proof.

val thmProof = x2nExpr .symWit.liftWit (g :-> leq(l(g))(thmBound))(exprBound)
val x2n = FreeGroup.power(x)(NatRing.prod(n)(nat(2)))
assert(thmProof.typ == leq(l(x2n))(thmBound ))

git commit hash when running tutorial: dba44cb5339f5c1c12afb49af558764c8efd887c