Suppose you put unit quaternions $q_0, q_1, q_2, q_3, q_4$ at the vertices of a regular 4-simplex.  Assume $q_0 = 1$.  Let the other four generate a group via quaternion multiplication.  Is this a free group on 4 generators?

I heard from Adrian Ocneanu that the answer is _yes_, but I don't know a proof.

Here's why I care.  As shown in this image by Greg Egan, you can inscribe a cube in a regular dodecahedron:

![twin dodecahedra][1]

 If you rotate the cube 90 degrees about an axis of 4-fold symmetry, the dodecahedron will be mapped to a _different_ dodecahedron.  Ocneanu calls this a **twin** of the original dodecahedron.  Despite the name, a regular dodecahedron actually has 5 different twins, one for each cube that can be inscribed in it.  

You can create a graph as follows. Start with a node for our original dodecahedron. Draw nodes for all the dodecahedra you can get from this one by repeatedly taking twins. Connect two nodes with an edge if and only if they are twins of each other.

Ocneanu claims the resulting graph is a tree! In other words, if you start at your original dodecahedron, and keep walking along edges of this graph by taking twins, you’ll never get back to where you started except by undoing all your steps.

Ocneanu didn't tell me the proof, but he said the key to the proof was this: 

**Claim**: if you take unit quaternions at the vertices of a regular 4-simplex, one of them equal to 1, the remaining four are generators of free group. 

Indeed, Egan and I were able to use this claim to prove that the graph is a tree:

* John Baez, [Twin dodecahedra](http://blogs.ams.org/visualinsight/2015/05/01/twin-dodecahedra/), _Visual Insight_ 1 May 2015.

So now I want to know why Ocneanu's claim is true --- and indeed, I want to _that_ it is true.

If it helps, you can assume the regular 4-simplex has these vertices:

$$ q_0 = 1 $$

$$q_1 = -\frac{1}{4} + \frac{\sqrt{5}}{4} i + \frac{\sqrt{5}}{4} j +  \frac{\sqrt{5}}{4} k  $$

$$ q_2 = -\frac{1}{4} +  \frac{\sqrt{5}}{4} i -\frac{\sqrt{5}}{4} j -\frac{\sqrt{5}}{4} k $$

$$ q_3 = -\frac{1}{4} -\frac{\sqrt{5}}{4} i + \frac{\sqrt{5}}{4} j -\frac{\sqrt{5}}{4} k $$

$$ q_4 = -\frac{1}{4}  -\frac{\sqrt{5}}{4} i -\frac{\sqrt{5}}{4}  j   +\frac{\sqrt{5}}{4} k $$


  [1]: https://i.sstatic.net/wqK0t.gif