Do unit quaternions at vertices of a regular 4-simplex, one being 1, generate a free group? Choose unit quaternions $q_0, q_1, q_2, q_3, q_4$ that form the vertices of a regular 4-simplex in the quaternions.  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:

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.  For example, the red dodecahedron above has the blue one as a twin, and vice versa.  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 a 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 know 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 $$
 A: By Stalling's theorem any torsion free virtually free group is free see here. By Ian Agol's answer the group is virtually free. 
All four quaternions are congruent to $-1/4$ mod $\sqrt 5$ and since $5/4-1/4=1$ as few-reps has noted in his or her answer they are all congruent to $1$. So their finite products are always congruent to a non-zero real number mod $\sqrt 5$. So the sum of their squares is a fraction with relatively prime denominator and numerator,with the numerator divisible by 5. 
Now the real term of any quaternion is the cosine of the angle through which quaternion rotates the plane consisting of the two vectors with zero real terms which are perpendicular to the non-real part of the quaternion. For this to have a prime power equal to one the angle of rotation must be rational.
Now here we have a classification of all rational and all quadratic values for cosines of rational angles they are $0$, $\pm 1/2$, $\pm 1$ and also some terms involving square roots of two or three which can be ignored and finally $\pm 1/4 \pm (\sqrt 5)/4)$. 
Now we can look at these cases individually for the real part equals $1$ that is the identity and that does not contribute to torsion, for $1/2$ the sum of the squares of the non-real components will not equal a fraction with relatively prime denominator and numerator,with the numerator divisible by $5$, for zero the real component is zero when by the above it must be 
non zero.
For the real part equals $\pm 1/4 \pm (\sqrt 5)/4)$  the squares of the non=real components will not equal a fraction with relatively prime denominator and numerator,with the numerator divisible by $5$.
Finally if we have real part equal to $-1$ we note it does not equal $1$ mod square root of 5. 
So we have covered all cases and there is no torsion and if the group is virtually free it is free.
A: Have you seen the preprint by Adrian Ocneanu?  It has been available since May 13; he has these proofs worked out in full detail.  See http://arxiv.org/abs/1505.03248.
A: Edit: The previous answer had an error, which I realized from a comment of @Will Sawin, and I've completely revised it. 
This group is a subgroup of an S-arithmetic lattice, which acts discretely on finite-valence Serre tree associated to $SL_2$ (really, a Bruhat-Tits building associated to $SL_2(F)$, where $F$ is a local field), hence is virtually free. 
The rational quaternions is a quaternion algebra with Hilbert symbol $\binom{\underline{-1,-1}}{\mathbb{Q}}$. We may tensor with $F=\mathbb{Q}(\sqrt{5})$
to get the quaternion algebra $A=\binom{\underline{-1,-1}}{F}$. The given elements $q_i$ are unit norm elements in the quaternion algebra $A$.
Since the real quaternions $\binom{\underline{-1,-1}}{\mathbb{R}}$ is ramified
(i.e. a division algebra), the algebra $\binom{\underline{-1,-1}}{F}$ is ramified at both real places (tensoring $A$ with $\mathbb{R}$ over the two embeddings of $F$ into $\mathbb{R}$. 
For all odd places (i.e. tensoring $A$ with $F_\mathcal{P}$, the $\mathcal{P}$-adic completion of $F$), the quaternion algebra $A_\mathcal{P}=A\otimes_F F_\mathcal{P}$ splits, i.e. is isomorphic to a matrix algebra $M_2(F_\mathcal{P})$. Since $2$ does not split over $F$, the algebra $A_{(2)}$ must also split, since $A$ must split at an even number of places by Hilbert's Reciprocity Law. 
The given elements lie in an order $\mathbb{Z}[\sqrt{5}][\frac12][1,i,j,k] \subset A$. For each odd prime $\mathcal{P}$, this lies in a compact subgroup of $A_\mathcal{P}$, and lies in a compact subgroup of the real places. So it must be a lattice in $A_{(2)}^1\cong SL_2(F_{(2)})$. Therefore, it acts on the tree associated to $SL_2(F_{(2)})$, described in Serre's book Trees Chapter II.1 (this is the Bruhat-Tits building associated to $SL_2(F_{(2)})$). 
 Thus, the group is virtually free.
The residue field  of $\mathcal{O}_{F_{(2)}}$ is $\mathbb{Z}[(1+\sqrt{5})/2]/(2)=\mathbb{F}_4$, the field with 4 elements, so the Serre tree has degree 5 ($=|\mathbb{P^1F}_4|$). It is tempting to guess that vertices of the Serre tree will correspond to dodecahedra, and neighbors to twins, but I haven't checked this. However, it's clear that the automorphism group $A_5$ of the dodecahedron stabilizes a vertex of the Serre tree, and the twin dodecahedra should have automorphism group stabilizing adjacent vertices of the tree.
