I recently found out about the discovery of 13 beautiful periodic solutions to the three-body problem, described in the paper
I am particularly impressed by how elaborate the solutions are, and I'm struck by the tantalizing hint of an infinity of other distinct orbits given by the analogy with a free group. The solutions can be viewed in the Three-Body Galery, which has animations of the new orbits in real space and in something called the 'shape sphere', which is described in the paper.
I was aware already of the figure-of-eight solution, which is described nicely in
A new solution to the three body problem - and more. Bill Casselman. AMS Feature Column.
and which was discovered numerically by Christopher Moore (Phys. Rev. Lett. 70, 3675 (1993)). I understand that the figure-of-eight solution has been proven to actually exist as a solution of the ODE problem, in
A Remarkable Periodic Solution of the Three-Body Problem in the Case of Equal Masses. Alain Chenciner and Richard Montgomery. Ann. Math 152 no. 3 (2000), pp. 881-901.
There is also a large class of solutions called $N$-body choreographies by Carles Simó, in which a number of bodies - possibly more than three - all follow the same curve. Simó found a large class of them in 2000 (DOI/pdf), though this nice review (DOI) seems to imply that formal theorematic proof that they exist as periodic solutions of the ODE problem is still lacking.
So, this brings me to my actual question. For the numerical simulations, however well you do them, in the end you will only have a finite-precision approximation to a solution of a differential equation that is propagated for a finite time. Additionally, you might do a numerical stability analysis that strongly suggests (or rigorously proves?) that you are (or are not) in a stable orbit. However, this is quite a ways away from a rigorous existence theorem for a periodic orbit with that symmetry.
With this in mind, then, in what spirit are these simulations done? Is it purely a numerical approach, in the hope that good numerics do indicate existence, but with a rigorous proof left to the mathematicians through whatever other means they can manage? Or is there some overarching theorem that indicates the existence of a truly periodic solution after a given threshold? What tools are there for proving existence theorems of periodic solutions?