  We prove the uniqueness of several excited states to the ODE $\ddot y(t) +
\frac{2}{t} \dot y(t) + f(y(t)) = 0$, $y(0) = b$, and $\dot y(0) = 0$ for the
model nonlinearity $f(y) = y^3 - y$. The $n$-th excited state is a solution
with exactly $n$ zeros and which tends to $0$ as $t \to \infty$. These
represent all smooth radial nonzero solutions to the PDE $\Delta u + f(u)= 0$
in $H^1$. We interpret the ODE as a damped oscillator governed by a double-well
potential, and the result is proved via rigorous numerical analysis of the
energy and variation of the solutions. More specifically, the problem of
uniqueness can be formulated entirely in terms of inequalities on the solutions
and their variation, and these inequalities can be verified numerically.
