# A formal proof

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 the ProvingGround project.

## The statement

Assume we are given the following:

• A group $G$.
• A (length) function $l: G \to \mathbb{Q}$ such that
• For $g, h \in G$, $l(gh) \leq l(g) + l(h)$,
• For $g, h\in G$, $l(ghg^{-1}) = l(g$).
• Elements $x, y, z, w \in G$ such that
• $x \sim yw$ (here $\sim$ means conjugate in $G$),
• $x \sim zw^{-1}$.

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.

scala> import provingground._, HoTT._
import provingground._
import HoTT._

scala> import functionfinder._, andrewscurtis.FreeGroups._
import functionfinder._
import andrewscurtis.FreeGroups._

scala> import spire.implicits._
import spire.implicits._

scala> import NatRing.{ x=>_,  Literal => nat, _}, QField.{w => _, x =>_, y=>_, z=>_, Literal => rat, _}, FreeGroup.{Literal => elem, _}
import NatRing.{x=>_, Literal=>nat, _}
import QField.{w=>_, x=>_, y=>_, z=>_, Literal=>rat, _}
import FreeGroup.{Literal=>elem, _}

scala> import Theorems.{PowerDistributive, ConjPower}
import Theorems.{PowerDistributive, ConjPower}


## The Setup

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

scala> val l = "l" :: FreeGroup ->: QTyp
l: provingground.HoTT.Func[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word],provingground.functionfinder.RepTerm[spire.math.Rational]] with provingground.HoTT.Subs[provingground.HoTT.Func[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word],provingground.functionfinder.RepTerm[spire.math.Rational]]] = l

scala> val g = "g" :: FreeGroup
g: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = g

scala> val h = "h" :: FreeGroup
h: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = h

scala> val n = "n" :: NatTyp
n: provingground.functionfinder.RepTerm[spire.math.SafeLong] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[spire.math.SafeLong]] = n

scala> val triang =
|   "triangle-inequality" :: (
|     g ~>: (h ~>: (
|       (leq(l(g |+| h))(l(g) + l(h)))
|     ))
|   )
triang: provingground.HoTT.FuncLike[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]],provingground.HoTT.FuncLike[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]],provingground.functionfinder.QField.PosWit]] with provingground.HoTT.Subs[provingground.HoTT.FuncLike[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]],provingground.HoTT.FuncLike...

scala> val conjInv =
|   "conjugacy-invariance" :: (
|     g ~>: (
|       h ~>: (
|         (l(h) =:= (l(g |+| h |+| g.inverse)))
|       )
|     )
|   )
conjInv: provingground.HoTT.FuncLike[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]],provingground.HoTT.FuncLike[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]],provingground.HoTT.Equality[provingground.functionfinder.RepTerm[spire.math.Rational]]]] with provingground.HoTT.Subs[provingground.HoTT.FuncLike[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis....


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}$.

scala> val w = "w" :: FreeGroup
w: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = w

scala> val y = "y" :: FreeGroup
y: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = y

scala> val z = "z" :: FreeGroup
z: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = z

scala> val s = "s" :: FreeGroup
s: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = s

scala> val t = "t" :: FreeGroup
t: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = t


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.

scala> val wy = w |+| y
wy: provingground.functionfinder.FreeGroup.LocalTerm = ((mul) (w)) (y)

scala> val zwbar = z |+| w.inverse
zwbar: provingground.functionfinder.FreeGroup.LocalTerm = ((mul) (z)) ((inv) (w))

scala> val wyn = FreeGroup.power(wy)(n)
wyn: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] = (<function1>) (n)

scala> val zwbarn = FreeGroup.power(zwbar)(n)
zwbarn: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] = (<function1>) (n)

scala> val c = n :-> (wyn |+| s.inverse |+| t |+| zwbarn) // this is the function we have to bound.
c: provingground.HoTT.Func[provingground.functionfinder.RepTerm[spire.math.SafeLong] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[spire.math.SafeLong]],provingground.functionfinder.FreeGroup.LocalTerm] = (n :  Nat.Typ) ↦ (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))

scala> val r = incl(QField)
r: provingground.functionfinder.NatRing.Rec[provingground.functionfinder.QField.LocalTerm] = <function1>

scala> val f = n :-> (l(s.inverse) + l(t) + ((l(y) + l(z)) * r(n) ) )
f: provingground.HoTT.Func[provingground.functionfinder.RepTerm[spire.math.SafeLong] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[spire.math.SafeLong]],provingground.functionfinder.QField.LocalTerm] = (n :  Nat.Typ) ↦ (((l) (t) + (l) ((inv) (s)) + ((<function1>) (n) * (l) (z)) + ((<function1>) (n) * (l) (y))))

scala> val lemma = n :-> (leq (l(c(n)) )(f(n) ) )
lemma: provingground.HoTT.Func[provingground.functionfinder.RepTerm[spire.math.SafeLong] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[spire.math.SafeLong]],provingground.functionfinder.QField.Pos] = (n :  Nat.Typ) ↦ (Pos((((l) (z) * (<function1>) (n)) + ((prod) (-1)) ((l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + (l) ((inv) (s)) + ((<function1>) (n) * (l) (y)) + (l) (t))))


## 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.

scala> val d = n :-> (wy |+| wyn |+| s.inverse |+| t |+| zwbarn  |+| zwbar)
d: provingground.HoTT.Func[provingground.functionfinder.RepTerm[spire.math.SafeLong] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[spire.math.SafeLong]],provingground.functionfinder.FreeGroup.LocalTerm] = (n :  Nat.Typ) ↦ (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))

scala> val dIsc = FreeGroup.rm(s.inverse |+| t |+| zwbarn |+| zwbar) *: (PowerDistributive.pf(wy)(nat(1))(n))
dIsc: provingground.HoTT.Equality[provingground.functionfinder.FreeGroup.LocalTerm] = (ind{($avmbv : FreeGroup) ↦ (($avmbw :  FreeGroup) ↦ ($avmbv =$avmbw))(((mul) (w)) (((mul) (y)) ((<function1>) (n))))(((mul) ((<function1>) (n))) (((mul) (w)) (y)))}{($asamy : FreeGroup) ↦ (($asamz :  FreeGroup) ↦ ((_ : ($asamy =$asamz) :  $asamy =$asamz) ↦ (((mul) ($asamy)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))) = ((mul) ($asamz)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))}(($asamy : FreeGroup) ↦ (Refl(FreeGroup,((mul) ($asamy)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))))))) ((<function1>) (n) : (((mul) (w)) (((mul) (y...

scala> 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)).

scala> val b = n :-> (y |+| wyn |+| s.inverse |+| t |+| zwbarn  |+| z)
b: provingground.HoTT.Func[provingground.functionfinder.RepTerm[spire.math.SafeLong] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[spire.math.SafeLong]],provingground.functionfinder.FreeGroup.LocalTerm] = (n :  Nat.Typ) ↦ (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z))))))

scala> val lbIsld = conjInv(w)(y |+| c(n) |+| z)
lbIsld: provingground.HoTT.Equality[provingground.functionfinder.RepTerm[spire.math.Rational]] = ((conjugacy-invariance) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) : ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))) = (l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))

scala> val bIsc = lbIsld && (l *: dIsc)
bIsc: provingground.HoTT.Equality[provingground.functionfinder.RepTerm[spire.math.Rational] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[spire.math.Rational]]] = ((ind{($bkqmt : Q.Typ) ↦ (($bkqmu :  Q.Typ) ↦ ($bkqmt =$bkqmu))((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))))((l) (((mul) (w)) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))}{($azfrn : Q.Typ) ↦ (($azfro :  Q.Typ) ↦ ((_ : ($azfrn =$azfro) :  $azfrn =$azfro) ↦ (($azfro = (l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w)))))... scala> 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. scala> val baseCase = triang(inv(s))(t) !: (lemma(0)) baseCase: provingground.functionfinder.QField.PosWit = ((triangle-inequality) ((inv) (s))) (t) : (Pos((((prod) (-1)) ((l) (((mul) ((inv) (s))) (t))) + (l) ((inv) (s)) + (l) (t))))  The induction step takes more work. We first assume the induction hypothesis. scala> val hyp = "hyp" :: lemma(n) hyp: provingground.functionfinder.QField.PosWit with provingground.HoTT.Subs[provingground.functionfinder.QField.PosWit] = hyp : (Pos((((prod) (-1)) ((l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + (l) ((inv) (s)) + ((l) (z) * (<function1>) (n)) + (l) (t) + ((<function1>) (n) * (l) (y)))))  Next, we bound$l(b(n))$(which we know is$l(c(n+ 1)))$in terms of$l(c(n))$. scala> val lbnBoundedlcnlylz = triang(y)(c(n)) + triang(y |+| c(n))(z) lbnBoundedlcnlylz: provingground.functionfinder.QField.PosWitSum = PosWitSum(((triangle-inequality) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))) : (Pos((((prod) (-1)) ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) + (l) (y) + (l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))))),((triangle-inequality) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) (z) : (Pos((((prod) (-1)) ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z))))))) + (l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) ... scala> 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))$. scala> val lbnBounded = lbnBoundedlcnlylz + hyp lbnBounded: provingground.functionfinder.QField.PosWitSum = PosWitSum(PosWitSum(((triangle-inequality) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))) : (Pos((((prod) (-1)) ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) + (l) (y) + (l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))))),((triangle-inequality) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) (z) : (Pos((((prod) (-1)) ((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z))))))) + (l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mu... scala> 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))$. scala> val bnd = "bound" :: QField.LocalTyp bnd: provingground.functionfinder.RepTerm[spire.math.Rational] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[spire.math.Rational]] = bound scala> val cbnd = bIsc.lift(bnd :-> (leq(bnd)(f(succ(n)) ) )) cbnd: provingground.HoTT.Func[provingground.functionfinder.QField.PosWit,provingground.functionfinder.QField.PosWit] = (ind{($dbysx :  Q.Typ) ↦ (($dbysy : Q.Typ) ↦ ($dbysx = $dbysy))((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))))((l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))}{($bkxqb :  Q.Typ) ↦ (($bkxqc : Q.Typ) ↦ ((_ : ($bkxqb = $bkxqc) :$bkxqb = $bkxqc) ↦ ((Pos((((prod) (-1)) ($bkxqb) + (l) (y) + (l) ((inv) (s)) + (l) (z) + ((l) (z) * (<function1>) (n)) + (l) (t) + ((<function1>) (n) * (l) (y))))) → (Pos(((l) (y) + ((prod) (-1)) ($bkxqc) + (l) ((inv) (s)) + (l) (z) + ((l) (z) ... scala> val step = cbnd(lbnBounded) step: provingground.functionfinder.QField.PosWit = ((ind{($dbysx :  Q.Typ) ↦ (($dbysy : Q.Typ) ↦ ($dbysx = $dbysy))((l) (((mul) (y)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (z)))))))((l) (((mul) ((<function1>) (n))) (((mul) (w)) (((mul) (y)) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) (((mul) (z)) ((inv) (w))))))))))}{($bkxqb :  Q.Typ) ↦ (($bkxqc : Q.Typ) ↦ ((_ : ($bkxqb = $bkxqc) :$bkxqb = $bkxqc) ↦ ((Pos((((prod) (-1)) ($bkxqb) + (l) (y) + (l) ((inv) (s)) + (l) (z) + ((l) (z) * (<function1>) (n)) + (l) (t) + ((<function1>) (n) * (l) (y))))) → (Pos(((l) (y) + ((prod) (-1)) ($bkxqc) + (l) ((inv) (s)) + (l) (z) + ((l) (z) * (<function1>) (n)) + (l) (t) + ((<function1>) (n) * (l) (y)))))))... scala> assert(step.typ == lemma(succ(n)))  Finally, the lemma is proved by induction. scala> val lemmaProof = Induc(lemma, baseCase, n :~> (hyp :-> step)) lemmaProof: provingground.functionfinder.NatRing.Induc[provingground.functionfinder.QField.PosWit with provingground.HoTT.Subs[provingground.functionfinder.QField.PosWit]] = <function1> scala> 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}$scala> val x = "x" :: FreeGroup x: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = x scala> val g = "g" :: FreeGroup g: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = g scala> val pown = g :-> FreeGroup.power(g)(n) pown: provingground.HoTT.Func[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]],provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]] = (g : FreeGroup) ↦ ((<function1>) (n)) scala> val c1 = "x ~ wy" :: (x =:= (s |+| w |+| y |+| s.inverse)) c1: provingground.HoTT.Equality[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]]] with provingground.HoTT.Subs[provingground.HoTT.Equality[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]]]] = x ~ wy : (x = ((mul) (s)) (((mul) (w)) (((mul) (y)) ((inv) (s))))) scala> val c2 = "x ~ zw^{-1}" :: (x =:= (t |+| z |+| w.inverse |+| t.inverse)) c2: provingground.HoTT.Equality[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]]] with provingground.HoTT.Subs[provingground.HoTT.Equality[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]]]] = x ~ zw^{-1} : (x = ((mul) (t)) (((mul) (z)) (((mul) ((inv) (w))) ((inv) (t)))))  We deduce using a theorem (in our code) about powers of conjugates that$x^n = s(wy)^ns^{-1} = t(zw^{-1})^nt^{-1}$. scala> val xnConjwyn = (pown *: c1) && ConjPower.pf(s)(wy)(n) xnConjwyn: provingground.HoTT.Equality[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]]] = ((ind{($dgjlv :  FreeGroup) ↦ (($dgjlw : FreeGroup) ↦ ($dgjlv = $dgjlw))((<function1>) (n))((<function1>) (n))}{($dfdxi :  FreeGroup) ↦ (($dfdxj : FreeGroup) ↦ ((_ : ($dfdxi = $dfdxj) :$dfdxi = $dfdxj) ↦ (($dfdxj = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) → ($dfdxi = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))))))}(($dfdxi :  FreeGroup) ↦ (($dfely : ($dfdxi = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) :  $dfdxi = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s)))) ↦ ($dfely : ($dfdxi = (... scala> val xnConjzwbarn= (pown *: c2) && ConjPower.pf(t)(zwbar)(n) xnConjzwbarn: provingground.HoTT.Equality[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] with provingground.HoTT.Subs[provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word]]] = ((ind{($difot :  FreeGroup) ↦ (($difou : FreeGroup) ↦ ($difot = $difou))((<function1>) (n))((<function1>) (n))}{($dgyvm :  FreeGroup) ↦ (($dgyvn : FreeGroup) ↦ ((_ : ($dgyvm = $dgyvn) :$dgyvm = $dgyvn) ↦ (($dgyvn = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))) → ($dgyvm = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))}(($dgyvm :  FreeGroup) ↦ (($dgzkc : ($dgyvm = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))) :  $dgyvm = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))) ↦ ($dgzkc : ($dgyvm ... scala> assert(xnConjwyn.typ == (pown(x) =:= (s |+| pown(wy) |+| s.inverse ) ) ) scala> 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}$. scala> val t1 = s |+| pown(wy) |+| s.inverse t1: provingground.functionfinder.FreeGroup.LocalTerm = ((mul) (s)) (((mul) ((<function1>) (n))) ((inv) (s))) scala> val t2 = t |+| pown(zwbar) |+| t.inverse t2: provingground.functionfinder.FreeGroup.LocalTerm = ((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))) scala> val xnxnExpr = (FreeGroup.rm(pown(x)) *: xnConjwyn) && (FreeGroup.lm(t1) *: xnConjzwbarn) xnxnExpr: provingground.HoTT.Equality[provingground.functionfinder.FreeGroup.LocalTerm with provingground.HoTT.Subs[provingground.functionfinder.FreeGroup.LocalTerm]] = ((ind{($dreuw :  FreeGroup) ↦ (($dreux : FreeGroup) ↦ ($dreuw = $dreux))(((mul) ((<function1>) (n))) ((<function1>) (n)))(((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) ((<function1>) (n)))))}{($dmftf :  FreeGroup) ↦ (($dmftg : FreeGroup) ↦ ((_ : ($dmftf = $dmftg) :$dmftf = $dmftg) ↦ (($dmftg = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) → ($dmftf = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))))))}(($dmftf :  FreeGroup) ↦ (($dm... scala> 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}$. scala> val x2nExpr =PowerDistributive.pf(x)(n)(n).sym && xnxnExpr x2nExpr: provingground.HoTT.Equality[provingground.functionfinder.FreeGroup.LocalTerm with provingground.HoTT.Subs[provingground.functionfinder.FreeGroup.LocalTerm] with provingground.HoTT.Subs[provingground.functionfinder.FreeGroup.LocalTerm with provingground.HoTT.Subs[provingground.functionfinder.FreeGroup.LocalTerm]]] = ((ind{($dtucf :  FreeGroup) ↦ (($dtucg : FreeGroup) ↦ ($dtucf = $dtucg))((<function1>) (((prod) (2)) (n)))(((mul) ((<function1>) (n))) ((<function1>) (n)))}{($drtzk :  FreeGroup) ↦ (($drtzl : FreeGroup) ↦ ((_ : ($drtzk = $drtzl) :$drtzk = $drtzl) ↦ (($drtzl = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t))))))) → ($drtzk = ((mul) (s)) (((mul) ((<function1>) (n))) (((mul)... scala> 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}$. scala> val thmBound = f(n) + l(s) + l(t.inverse) thmBound: provingground.functionfinder.QField.LocalTerm = ((l) (s) + (l) ((inv) (s)) + (l) ((inv) (t)) + ((l) (z) * (<function1>) (n)) + (l) (t) + ((<function1>) (n) * (l) (y))) scala> val exprBound = lemmaProof(n) + triang(s)(c(n)) + triang(s |+| c(n))(t.inverse) exprBound: provingground.functionfinder.QField.PosWitSum = PosWitSum(PosWitSum((<function1>) (n) : (Pos((((prod) (-1)) ((l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)))))) + (l) ((inv) (s)) + ((l) (z) * (<function1>) (n)) + (l) (t) + ((<function1>) (n) * (l) (y))))),((triangle-inequality) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))) : (Pos((((prod) (-1)) ((l) (((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))) + (l) (s) + (l) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n))))))))),((triangle-inequality) (((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) ((<function1>) (n)... scala> assert(exprBound.typ == leq(l(s |+| c(n) |+| t.inverse ))(thmBound))  We easily deduce the bound on$l(x^{2n})$to complete the proof. scala> val thmProof = x2nExpr.sym.lift (g :-> leq(l(g))(thmBound))(exprBound) thmProof: provingground.functionfinder.QField.PosWit = ((ind{($fkgdm :  FreeGroup) ↦ (($fkgdn : FreeGroup) ↦ ($fkgdm = $fkgdn))(((mul) (s)) (((mul) ((<function1>) (n))) (((mul) ((inv) (s))) (((mul) (t)) (((mul) ((<function1>) (n))) ((inv) (t)))))))((<function1>) (((prod) (2)) (n)))}{($dxkkp :  FreeGroup) ↦ (($dxkkq : FreeGroup) ↦ ((_ : ($dxkkp = $dxkkq) :$dxkkp = $dxkkq) ↦ ((Pos(((l) (s) + ((prod) (-1)) ((l) ($dxkkp)) + (l) ((inv) (s)) + (l) ((inv) (t)) + ((l) (z) * (<function1>) (n)) + (l) (t) + ((<function1>) (n) * (l) (y))))) → (Pos(((l) (s) + (l) ((inv) (s)) + (l) ((inv) (t)) + ((l) (z) * (<function1>) (n)) + ((prod) (-1)) ((l) ($dxkkq)) + (l) (t) + ((<function1>) (n) * (l) (y))))))))}(($dxkkp :  FreeGroup) ↦ ((\$ejnjf : (Pos(((l) (s) + (l) ((inv) (s)) +...

scala> val x2n = FreeGroup.power(x)(NatRing.prod(n)(nat(2)))
x2n: provingground.functionfinder.RepTerm[provingground.andrewscurtis.FreeGroups.Word] = (<function1>) (((prod) (2)) (n))

scala> assert(thmProof.typ == leq(l(x2n))(thmBound ))