Edit: Added proof that the 4-simplex generates a free group.
Here's a fairly simple proof that the graph of twin dodecahedra is a tree, which is then used to prove that the 4-simplex generates a free group.
We'll start by working with a graph of twin 4-simplexes, rather than twin dodecahedra. (This is an approach that John Baez suggested.) Given any 4-simplex with five unit quaternions $q_i$ as its vertices, we will define five "twins" of this 4-simplex, relative to each of its five vertices, as the 4-simplexes with vertices:
$$q^{(m)}_i = q_m q_i^{-1} q_m$$
When $q_m = q_i$ we have:
$$q^{(m)}_m = q_m$$
So the simplex and its twin always share a vertex. If we then "twinned" the twin simplex relative to that shared vertex, we would be taken back to the original simplex:
$$q^{(m)}_m (q^{(m)}_i)^{-1} q^{(m)}_m = q_m q_m^{-1} q_i q_m^{-1} q_m = q_i$$
We will define a map $G: \mathbb{Q}^4 \to \mathbb{Q}(\sqrt{5})^4$ as:
$$G(x) = \left(x_0, x_1 \sqrt{5}, x_2 \sqrt{5}, x_3 \sqrt{5}\right)$$
Now suppose we have unit quaternions:
$$q_a = G(a) \qquad q_b = G(b)$$
where $a, b \in \mathbb{Q}^4$, and $q_a$ and $q_b$ are distinct vertices of the same 4-simplex, so that $q_a \cdot q_b = -\frac{1}{4}$. Then the quaternion multiplications of the twinning operation simplify to an extraordinary extent, and we have:
$$q_a q_b^{-1} q_a = -\frac{1}{2} G(a+2b)\qquad q_a \ne q_b$$
(If $q_a = q_b$, then of course the twin itself is simply equal to $q_a$.)
Let's further suppose that all $a_i, b_i$ are equal to integers divided by powers of 2, and that we write each unit quaternion $q_a$ and $q_b$ with a common denominator across all four components:
$$q_a = \frac{1}{2^{n_a}} G(r)$$
$$q_b = \frac{1}{2^{n_b}} G(s)$$
where $r, s \in \mathbb{Z}^4$, and at least one of the $r_i$ and at least one of the $s_i$ are odd.
We then have:
$$q_a q_b^{-1} q_a = -\frac{1}{2^{n_a+n_b+1}} G(2^{n_b}r+2^{n_a+1}s)$$
If $n_a+1 \gt n_b$, we can cancel a factor of $2^{n_b}$, giving us:
$$q_a q_b^{-1} q_a = -\frac{1}{2^{n_a+1}} G(r+2^{n_a-n_b+1}s)$$
Since at least one of the $r_i$ is odd, no further cancellation is possible.
If $n_a+1 \lt n_b$, we can cancel a factor of $2^{n_a+1}$, giving us:
$$q_a q_b^{-1} q_a = -\frac{1}{2^{n_b}} G(2^{n_b-n_a-1}r+s)$$
Since at least one of the $s_i$ is odd, no further cancellation is possible.
If $n_a+1 = n_b$, we have:
$$q_a q_b^{-1} q_a = -\frac{1}{2^{n_b}} G(r+s)$$
Here it's possible that there will be further cancellation, depending on the details of the $r_i$ and $s_i$. However, it will turn out that we'll never need to make use of this case, because it only shows up if we move backwards through the graph.
So $n_t$, the power of 2 in the denominator of the twin's vertex, will be:
$$n_t=\begin{cases}
max(n_a+1,n_b) & n_a+1 \ne n_b \\
n_b - ? & n_a+1 = n_b\end{cases}$$
In the original simplex, one of the vertices has $n=0$ as the power of 2 in its denominator, and the other four vertices have $n=2$. In its twins, we have the cases:
$$\begin{array}{cccc}
n_a & n_b & q_a = q_b & n_t \\
0 & 0 & T & 0 \\
0 & 2 & F & 2 \\
2 & 0 & F & 3 \\
2 & 2 & F & 3 \\
2 & 2 & T & 2 \end{array}$$
So the twin relative to the vertex $q_0=(1,0,0,0)$ has $n_t=0,2,2,2,2$ again, while those relative to the other vertices have $n_t=2,3,3,3,3$. But we only get $n_t=2$ when $q_a=q_b$, so as we extend the graph outwards we will never twin these twins relative to that vertex, since it would just take us back to the original simplex. This means that when we take twins of the twins, we don't encounter the case $n_b = n_a+1$, since in the first level twins we never set $q_a$ equal to the vertex with $n_t=2$.
As we take twins of twins, any sequence of powers we find starting from the twin with powers $0,2,2,2,2$ will just match one we find starting from the original simplex, so wlog we can assume we extend the graph through a twin with powers $2,3,3,3,3$. The possibilities are then:
$$\begin{array}{cccc}
n_a & n_b & q_a = q_b & n_t \\
3 & 2 & F & 4 \\
3 & 3 & F & 4 \\
3 & 3 & T & 3\end{array}$$
Once again, we will never take higher-level twins with the vertex we get from $q_a=q_b$, so again we avoid the case $n_b = n_a+1$. And it's clear now that the pattern will continue like this: every $n$th level twin (that we did not reach via $q_0$) will have powers $n+1,n+2,n+2,n+2,n+2$, while those that we did reach via $q_0$ will just look like $(n-1)$th level twins, with powers $n, n+1, n+1, n+1, n+1$.
If we choose a sequence $m_1, m_2, ... , m_M$ of vertices, with $m_k \ne m_{k+1}$, and apply the twinning operation repeatedly using the vertex with index $m_k$, for even $M$ we end up with:
$$q^{(m_1 m_2 ... m_M)}_i = q_{m_1} q_{m_2}^{-1} ... q_{m_M}^{-1} \: q_i \: q_{m_M}^{-1} ... q_{m_2}^{-1} q_{m_1}$$
while for odd $M$ we get:
$$q^{(m_1 m_2 ... m_M)}_i = q_{m_1} q_{m_2}^{-1} ... q_{m_M} \: q_i^{-1} \: q_{m_M} ... q_{m_2}^{-1} q_{m_1}$$
Now suppose that our graph was not a tree. Then there would be two different sequences of indexes like this, say $m_1, m_2, ... , m_M$ and $p_1, p_2, ... , p_P$ that resulted in the same simplex. We will define the rotation:
$$R(x) = q_{m_M}^{\pm 1} ... q_{m_2} q_{m_1}^{-1} \: x \: q_{m_1}^{-1} q_{m_2} ... q_{m_M}^{\pm 1}$$
where $q_{m_M}^{\pm 1} = q_{m_M}$ if $M$ is even, and $q_{m_M}^{-1}$ if $M$ is odd.
Applying $R$ to the first simplex will reduce it to either the original simplex, $q_i$, if $M$ is even, or to the twin relative to $q_0$, with vertices $q_i^{-1}$, if $M$ is odd.
If $M$ is even, applying $R$ to the second simplex will map it into the simplex that arises from the sequence $m_M, ..., m_1, p_1, ..., p_P$. If the two original sequences agree at the beginning, then $q_{m_1}^{-1}$ will cancel with $q_{p_1} = q_{m_1}$ in the string of vertex products, and so on for as long as the sequences are the same, but since the sequences are not identical, some non-empty sequence will remain.
If $M$ is odd, applying $R$ to the second simplex will map it into the inverse of the simplex that arises from the sequence $m_M, ..., m_1, p_1, ..., p_P$, again with some possible cancellations.
We then have the result that either the original simplex (if $M$ is even) or its inverse (if $M$ is odd), both of which have powers $0,2,2,2,2$, is equal to some other simplex in the graph (if $M$ is even), due to some non-empty sequence of twinning operations, or the inverse of that simplex (if $M$ is odd).
The only simplex in the graph, besides the original, with powers $0,2,2,2,2$ is the one due to the index sequence $0$: the twin of the original with respect to $q_0$. But we know this is the inverse of the original simplex, rather than being equal to it. Whether $M$ is even or odd, the claim ends up being that the original simplex and its inverse are equal, which is false. So our supposition that the graph is not a tree must be false.
Finally, we can relate this to the graph of dodecahedra as follows. Each simplex with vertices $q_i$ can be used to construct a dodecahedron, whose 20 vertices are:
$$d_{i,j} = q_i q_j^{-1} \qquad i \ne j$$
The dodecahedron constructed from a twin simplex has vertices:
$$d^{(m)}_{i,j} = q^{(m)}_i (q^{(m)}_j)^{-1} = q_m q_i^{-1} q_m (q_m q_j^{-1} q_m)^{-1} = q_m q_i^{-1} q_j q_m^{-1}$$
These share the 8 vertices where $i=m, j \ne m$ or $j=m, i \ne m$:
$$d^{(m)}_{m,j} = q_j q_m^{-1} = d_{j,m}$$
$$d^{(m)}_{i,m} = q_m q_i^{-1} = d_{m,i}$$
which makes them twin dodecahedra. So the tree of twin simplexes gives rise to a graph of twin dodecahedra.
The reason we can't immediately claim that the graph of dodecahedra is also a tree is that two non-identical simplexes can be used to construct the same dodecahedron. If we right-multiply all the vertices of a given simplex by the same unit quaternion $q_R$, rotating it into another simplex, then $q_R$ cancels out in the formula for the dodecahedron vertices.
So, could two of the simplexes in our tree be the same up to right multiplication by some quaternion $q_R$? We can show that this is impossible by exploiting the fact that all of these simplexes have their vertices in a particular subset of the golden field, $G(\mathbb{Q}^4) \subset \mathbb{Q}(\sqrt{5})^4$, in which the first coordinate is purely rational and all the other coordinates are rational multiples of $\sqrt{5}$.
Suppose we have three linearly independent, unit quaternions $q_i \in G(\mathbb{Q}^4)$, each of which is described in terms of a 4-vector of rationals, $a_i \in \mathbb{Q}^4$:
$$q_i = G(a_i) \qquad i=1,2,3$$
And suppose we pick some fourth quaternion, $p \in G(\mathbb{Q}^4)$, that we wish to map $q_1$ into by right multiplication, with $p = G(b)$ for some $b \in \mathbb{Q}^4$. The quaternion we need to right-multiply with to achieve this will be:
$$q_R = q_1^{-1} p$$
In general, $q_R$ will not belong to $G(\mathbb{Q}^4)$. The question we want to answer is: what restrictions are imposed on $p$ by requiring the images of the other $q_i$ under right multiplication:
$$q_i q_R = q_i q_1^{-1} p \qquad i=2,3$$
to lie in $G(\mathbb{Q}^4)$. Multiplying this out and setting the appropriate rational and irrational parts of the components of the product to zero, we obtain a set of eight linear equations in the rational parameters $b_j, j=0,1,2,3$:
$$\begin{array}{lcr}
b_3 \left(a_{1,2} a_{2,1}-a_{1,1} a_{2,2}\right)+b_2 \left(a_{1,1} a_{2,3}-a_{1,3} a_{2,1}\right)+b_1 \left(a_{1,3}
a_{2,2}-a_{1,2} a_{2,3}\right) & = & 0\\
b_3 \left(a_{1,0} a_{2,2}-a_{1,2} a_{2,0}\right)+b_2 \left(a_{1,3} a_{2,0}-a_{1,0} a_{2,3}\right)+b_0 \left(a_{1,2}
a_{2,3}-a_{1,3} a_{2,2}\right) & = & 0\\
b_3 \left(a_{1,1} a_{2,0}-a_{1,0} a_{2,1}\right)+b_1 \left(a_{1,0} a_{2,3}-a_{1,3} a_{2,0}\right)+b_0 \left(a_{1,3}
a_{2,1}-a_{1,1} a_{2,3}\right) & = & 0\\
b_2 \left(a_{1,0} a_{2,1}-a_{1,1} a_{2,0}\right)+b_1 \left(a_{1,2} a_{2,0}-a_{1,0} a_{2,2}\right)+b_0 \left(a_{1,1}
a_{2,2}-a_{1,2} a_{2,1}\right) & = & 0\\
b_3 \left(a_{1,2} a_{3,1}-a_{1,1} a_{3,2}\right)+b_2 \left(a_{1,1} a_{3,3}-a_{1,3} a_{3,1}\right)+b_1 \left(a_{1,3}
a_{3,2}-a_{1,2} a_{3,3}\right) & = & 0\\
b_3 \left(a_{1,0} a_{3,2}-a_{1,2} a_{3,0}\right)+b_2 \left(a_{1,3} a_{3,0}-a_{1,0} a_{3,3}\right)+b_0 \left(a_{1,2}
a_{3,3}-a_{1,3} a_{3,2}\right) & = & 0\\
b_3 \left(a_{1,1} a_{3,0}-a_{1,0} a_{3,1}\right)+b_1 \left(a_{1,0} a_{3,3}-a_{1,3} a_{3,0}\right)+b_0 \left(a_{1,3}
a_{3,1}-a_{1,1} a_{3,3}\right) & = & 0\\
b_2 \left(a_{1,0} a_{3,1}-a_{1,1} a_{3,0}\right)+b_1 \left(a_{1,2} a_{3,0}-a_{1,0} a_{3,2}\right)+b_0 \left(a_{1,1}
a_{3,2}-a_{1,2} a_{3,1}\right) & = & 0\end{array}$$
This system has a 1-parameter family of solutions:
$$b_i = \lambda a_{1,i}$$
In other words, the only vectors we can map $q_1$ into by right multiplication are scalar multiples of itself, if we want the images of $q_2$ and $q_3$ to lie in $G(\mathbb{Q}^4)$. So right multiplication can't map one of the simplexes in the tree into another, and each distinct simplex belongs in a distinct equivalence class modulo right multiplication.
This means the dodecahedra created from distinct simplexes in the tree are distinct, and the graph of dodecahedra is a tree.
To prove that the 4-simplex generates a free group, suppose we have any finite product of positive or negative powers of the elements $\{q_1, q_2, q_3, q_4\}$. By inserting the element 1 in the form $q_0$ or $q_0^{-1}$ where necessary, we can write this product as:
$$p=q_{m_1} q_{m_2}^{-1} q_{m_3} ... q_{m_M}^{\pm 1}$$
for some sequence $m_1, m_2, ... , m_M$ with $m_k \ne m_{k+1}$. We then have the vertices of the dodecahedron constructed from the 4-simplex associated with this sequence being, for even $M$:
$$d^{(m_1 m_2 ... m_M)}_{i,j} = p q_i q_j^{-1} p^{-1}$$
and for odd $M$:
$$d^{(m_1 m_2 ... m_M)}_{i,j} = p q_i^{-1} q_j p^{-1}$$
If $p=1$ for some non-empty sequence, then this dodecahedron would also appear elsewhere in the tree, either as the dodecahedron constructed from the original simplex, or the one constructed from its twin relative to $q_0$. But this is impossible, so $p \ne 1$.
