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. You can inscribe a cube in a regular dodecahedron. 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, 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 $$