Computer assisted proof of homoclinic chaos in the spatial equilateral restricted four-body problem

We develop constructive, computer assisted arguments for proving the existence of transverse homoclinic connections for hyperbolic periodic orbits in Hamiltonian systems. These arguments are applied at a number of non-perturbative parameter and energy values in the spatial equilateral circular restricted four-body problem: a six dimensional vector field. The idea is to formulate the desired connecting orbits as solutions of certain two point boundary value problems for orbit segments which originate and terminate on the local stable/unstable manifolds attached to a periodic orbit. These boundary value problems are studied via a Newton-Kantorovich argument in an appropriate Cartesian product of Banach algebras of rapidly decaying sequences of Chebyshev coefficients. Perhaps the most delicate part of the problem is controlling the boundary conditions, which must lie on the local stable/unstable manifolds of the periodic orbit. For this portion of the problem we use a parameterization method to develop Fourier-Taylor approximations equipped with mathematically rigorous a-posteriori error bounds. This requires validated computation of a finite number of Fourier-Taylor coefficients via Newton-Kantorovich arguments in appropriate Cartesian product of rapidly decaying sequences of Fourier coefficients, followed by a fixed point argument to bound the tail terms of the Taylor expansion. After some geometric considerations in the energy manifold, transversality of the connection follows as a direct consequence of the Newton-Kantorovich argument. (c) 2023 Elsevier Inc. All rights reserved.