Computer-assisted proof of skeletons of periodic orbits

When obtaining numerically invariants that describe the dynamics of a system, we are never sure about the real existence of that numerical objects. We propose to go further in the numerical search of periodic orbits, by performing a systematic computer-assisted proof of large sets of periodic orbits. First of all, we adapt the periodicity condition to a zero-finding criterion, so that we can apply validated numerical tools. This allows us to apply that criterion to a huge set of initial conditions (numerically calculated), to transform each numerical approach into a rigorous value. We show the figures representing periodic orbits, before and after validation, showing that these techniques allow to give, not only numerically calculated invariants that describe a system (skeleton of periodic orbits), but a rigorous result beyond its numerical description. Finally, we also show how to obtain a computer-assisted proof of the linear stability of the orbits.