Systematic Computer Assisted Proofs of periodic orbits of Hamiltonian systems

•A systematic approach to the Computer Assisted Proof of skeletons of periodic orbits of Hamiltonian systems is presented.•Numerical search of thousands of periodic orbits are converted in rigorous theorems via Computer Assisted Proof techniques.•Stability of these orbits is proved.•Continuous families of periodic orbits are proved via Computer Assisted Proof techniques using Chebyshev approximations.•Stability of families of periodic orbits is proved.

The numerical study of Dynamical Systems leads to obtain invariant objects of the systems such as periodic orbits, invariant tori, attractors and so on, that helps to the global understanding of the problem. In this paper we focus on the rigorous computation of periodic orbits and their distribution on the phase space, which configures the so called skeleton of the system. We use Computer Assisted Proof techniques to make a rigorous proof of the existence and the stability of families of periodic orbits in two-degrees of freedom Hamiltonian systems, which provide rigorous skeletons of periodic orbits. To that goal we show how to prove the existence and stability of a huge set of discrete initial conditions of periodic orbits, and later, how to prove the existence and stability of continuous families of periodic orbits. We illustrate the approach with two paradigmatic problems: the Hénon–Heiles Hamiltonian and the Diamagnetic Kepler problem.