Spatial periodic orbits in the equilateral circular restricted four-body problem: computer-assisted proofs of existence

Abstract

We use validated numerical methods to prove the existence of spatial periodic orbits in the equilateral restricted four-body problem. We study each of the vertical Lyapunov families (up to symmetry) in the triple Copenhagen problem, as well as some halo and axial families bifurcating from planar Lyapunov families. We consider the system with both equal and non-equal masses. Our method is constructive and non-perturbative, being based on a posteriori analysis of a certain nonlinear operator equation in the neighborhood of a suitable approximate solution. The approximation is via piecewise Chebyshev series with coefficients in a Banach space of rapidly decaying sequences. As by-product of the proof, we obtain useful quantitative information about the location and regularity of the solution.

1 Introduction

A complete understanding of the gravitational N-body problem is among the oldest challenges in mathematical physics, with roots in the age of Newton. In the nineteenth century, Poincaré initiated the study of the circular restricted three-body problem (CRTBP). In this simplified problem, two massive bodies (called primaries) are constrained to a fixed periodic solution of the Kepler problem, and a massless particle moves in their gravitational field. This is one of the simplest N-body problems which is not integrable and which admits chaotic motions. A complete review of the literature for the CRTBP is beyond the scope of this work, and we direct the interested reader to the watershed studies of Strömgren (1933), of Hénon (1965a, b), and of Broucke (1968). We also refer to the books of Moser (2001), of Szebehely (1967), of Meyer et al. (2009), and of Belbruno (2007) and also to the lecture notes of Chenciner (2015) for much more complete discussions.

The advent of space exploration in the twentieth century revitalized study of the CRTBP. Researchers developed new analytical and numerical techniques to find orbits for use in the design of space missions. One of the first works to study the possibility of using the R3BP to design space missions is found in the Ph.D. thesis of Farquhar (1968). He used some spatial periodic orbits in the CRTBP, the so-called halo orbits, as hypothetical locations for communications relay stations in the Apollo missions. The first mission to actually use a spatial halo orbit was the ISEE-3 satellite in 1978. Almost 20 years later, the Solar and Heliospheric Observatory (SOHO) was the second mission using this kind of orbit in 1996. Again a complete review of past and future missions considering halo orbits as trajectories is beyond the scope of this work, but it is worth mentioning that the James Webb Space Telescope—previously known as Next-Generation Space Telescope (NGST)—is tentatively scheduled to launch in 2021 and will be stationed on a halo orbit near the libration point $L_{2}$ in the Sun–Earth system. We refer to the interested reader to Folta and Beckman (2002) for further mission details.

Natural generalizations of the CRTBP consist in taking a special solution of the gravitational three-body problem and studying a massless particle moving in the resulting field. It is well known that the three-body problem admits an explicit solution known as the Lagrangian central configuration. This consists of three massive (not necessarily equal) bodies arranged in an equilateral triangle configuration. Each body moves in a periodic orbit of the Kepler problem, either elliptical or—as in our case—circular. The resulting four-body system is known as the equilateral circular restricted four-body problem (CRFBP).

Let us briefly consider some motivation for studying the CRFBP. Astronomical observations reveal that Lagrangian central configurations are found in our own Solar system. There are well-known examples of asteroids that lie approximately in an equilateral configuration in the Sun–Jupiter system. Such asteroids have been classified into two groups, the so-called Trojans and Greeks which both lie on the orbit of Jupiter. Trojan asteroids have been detected recently in our Solar system for the Mars–Sun and Neptune–Sun systems and even for the Earth–Sun system. We find equilateral triangle configurations also among Saturn and some of its moons, for example, Saturn–Tethys–Telesto, Saturn–Tethys–Calypso, or Saturn–Dione–Helene. Exploration of the Trojan asteroids was included with high priority in the 2013 Decadal Survey among the New Frontiers missions in the decade 2013–2022.

In Schwarz et al. (2007), the authors describe several observed extrasolar planetary systems (EPS) where they find a Sun-like star and a Jupiter-like gas giant orbiting the star. They compute the stability zones of hypothetical planets located approximately in an equilateral configuration formed by the star–gas giant-Trojan planet system. In other words, they consider hypothetical planets in a 1 : 1 orbital resonance with the gas giant. They also consider some other relevant effects in their work, related to the habitability of the Trojan planet. For example, they consider the age of the central star, the distance from it, climate considerations, etc.

Mathematical investigations of the CRFBP appear as early as the work of Pedersen (1944, 1952). A later study of Simó gave compelling numerical evidence for the conjecture that there are always eight, nine, or ten equilibrium solutions—depending on the mass ratios of the primary bodies (Simó 1978). The interested reader may want to consult also the study of Álvarez-Ramírez and Vidal (2009) where tools from the qualitative theory of dynamical systems are used to explore the phase space of the spatial problem in detail.

Rigorous mathematical proof of the correctness of the equilibrium count given by Simó in Simó (1978) has recently been completed in a series of papers by Leandro (2006), Barros and Leandro (2011, 2014). The proof uses Möbius transformations to put the problem into a form where the number of zeros is counted using rules of sign. From the point of view of the present discussion, it is important to mention that the proof is computer assisted.

The next simplest solutions of the CRFBP are periodic orbits, and these are studied in a number of works including Burgos-García (2016), Burgos-Garcia and Bengochea (2017), Burgos-García and Delgado (2013), Papadakis (2016), Baltagiannis and Papadakis (2011), and Papadakis (2016). The paper (Papadakis 2016) just cited is especially relevant to the present introduction, as the author studies some spatial families of periodic orbits in the CRFBP.

Inspired by the success of Leandro and Barros, we provide mathematically rigorous existence proofs for some spatial periodic orbits in the CRFBP. As in the works of Leandro and Barros, our method of proof is computer assisted. Of course, the number of periodic orbits in a Hamiltonian system is typically uncountable, and we cannot hope to obtain precise counts as in the equilibrium case. Instead, we focus on proving the existence of periodic orbits in certain prominent families like the vertical Lyapunov, halo, and axial solutions.

We present a method which can in principle be used to prove the existence of any non-degenerate periodic orbit for the CRFBP found using standard numerical methods. Here, non-degeneracy amounts to assuming that the periodic orbit is isolated in the energy level set and that it is not too close to a bifurcation. “Too close” involves implementation details like the number of digits of precision available in the representation of real numbers, the conditioning of certain matrices, and some local bounds on second derivatives.

Our arguments are based on a posteriori analysis in infinite sequence spaces of Chebyshev series coefficients. The method is constructive, works for parameter values far from any symmetric or perturbative special cases, and provides useful by-product such as precise bounds on the location of the orbits, bounds on derivatives, bounds on the domain of analyticity, and decay rates for the Chebyshev series coefficients of the periodic orbit. Some periodic orbits whose existence is proved using our methods are illustrated in Figs. 1, 2, and 3. More results are discussed in Sect. 5.

Fig. 1

Spatial periodic orbits in the triple Copenhagen problem: The figure illustrates 126 spatial periodic orbits in the equilateral restricted four-body problem with equal masses. Computer-assisted proofs of existence for these orbits—using the methods laid down in the present work—are discussed in Sect. 5. The triple Copenhagen problems have a $2\pi /3$ rotational symmetry, so that in this case we only have to prove one-third of the orbits and obtain the rest by symmetry

Fig. 2

Vertical Lyapunov families associated with libration points: The orbits illustrated in Fig. 1 are obtained by numerical continuation from the vertical families associated with the 10 libration points of the triple Copenhagen problem. Our method of proof is based on a posteriori analysis of numerical data and applies to any of the orbits located during the continuation. This figure illustrates the vertical families associated with $L_1$ (top frames) and $L_4$ (bottom frames). See Sect. 2 for an overview of the libration points and their stability

Fig. 3

Halo family in the equilateral restricted four-body problem: Spatial periodic orbits can appear as bifurcations from planar Lyapunov orbits. One such family is illustrated here for an equilateral restricted four-body problem with non-equal masses/broken symmetry. We refer to these as halo orbits, in analogy with similar families found in the CRTBP—an observer sitting in the xy-plane sees these as “halos” around a primary body. We discuss existence proofs for these and several related families bifurcating from the plane in Sect. 5

Our computer-assisted analysis builds on the earlier work of Hungria et al. (2016), Lessard et al. (2016), incorporating new developments due to Van den Berg and Sheombarsing (2016) (see Sect. 4), and Lessard (2018) (see Remark 4). Indeed, we defer to these references for many of the technical details and focus our attention instead on adapting these methods to the CRFBP and on the results so obtained.

Remark 1

(The functional analytic and phase space approaches) In Sect. 2.3, we briefly summarize several decades of mathematically rigorous computer-assisted analysis for N-body problems. In concluding the present introduction, we only remark that—very roughly speaking—existing work employs either topological arguments formulated in the phase space, or functional analytic arguments formulated in a Banach space.

The phase space methods depend on high-order Taylor/Lohner algorithms which track sets of initial conditions (Zgliczynski 2002). They apply degree theory—for example, Conley or Brouwer indices—to force the existence of non-trivial recurrent dynamics. The functional analytic methods reformulate invariant objects like equilibria, periodic orbits, smooth invariant manifolds, or connecting orbits as solutions of nonlinear operator equations. The equations may be discretized using Taylor, Fourier, Chebyshev, or Lindstedt series expansions, and a posteriori arguments based on implicit function theory force the existence of true solutions near good enough approximate ones.

From our point of view, the phase space/function space dichotomy is completely natural, as topological and analytical tools permeate every corner of dynamical systems theory. As the mathematically rigorous theory of computational dynamics evolves, it will necessarily grow in both directions. Matriculation of diverse approaches indicates health, rather than confusion, in our field.

The choice of a functional analytic framework for the present study is in part influenced by the taste of the authors, as well as by our desire to illustrate the successful use of these tool in an interesting and highly non-trivial application. An even more important factor is our desire to use these periodic orbits as the base step in constructing stable/unstable manifolds using the parameterization method (Cabré et al. 2003, 2005; Haro et al. 2016; Castelli et al. 2015). We are especially interested in combining the numerical methods developed in Mireles James and Murray (2017) with the a posteriori analysis developed in Castelli et al. (2018). The first step in this project is to numerically compute the periodic orbits using piecewise Chebyshev series equipped with validated truncation error bounds in the analytic category—exactly the problem solved in the present work. The resulting invariant manifold expansions, when combined with the analytic continuation techniques for local invariant manifolds developed in Kalies et al. (2018), Kepley and Mireles James (2018), lead to both computer-aided existence proofs for transverse connecting orbits and bounds on minimum transport times for these connections. We remark that while there exist many methods in the literature for proving the existence of connecting orbits (see the discussion in Sect. 2.3 for more references) only set-oriented methods like those of Kalies et al. (2018) and Kepley and Mireles James (2018) are able to rule out connections/bound minimum transport times.

The remainder of the paper is organized as follows. In Sect. 2, we review some background material pertaining to the a posteriori analysis. We also discuss briefly the rich literature on computer-assisted proof in Celestial Mechanics. In Sect. 3, we discuss a procedure which transforms our problem to polynomial and introduce appropriate phase conditions for periodic orbits in the transformed problem. In Sect. 4, we introduce the Chebyshev operator equation of the form $F(x)=0$ whose solutions correspond to periodic orbits of the CRFBP. Section 5 is devoted to results, where we prove existence of periodic orbits in the CRFBP by showing existence of solutions of $F=0$ using a rigorous computer-assisted a posteriori analysis.

2 Background

2.1 Equations of motion for the equilateral circular restricted four-body problem

We consider the motion of an infinitesimal particle, moving in the gravitational field of three massive bodies—the primaries—themselves moving in an equilateral triangular configuration of Lagrange. The equations of motion in a rotating frame are

$$\begin{aligned} {{\dot{{{\mathbf {x}}}}}} = f({{\mathbf {x}}}), \end{aligned}$$

where ${{\mathbf {x}}}(x, \dot{x}, y, \dot{y}, z, \dot{z})$ and with the vector field given by

$$\begin{aligned} f({{\mathbf {x}}}) \left( \begin{array}{c} \dot{x} \\ 2 \dot{y} + {\varOmega }_x(x, y, z) \\ \dot{y} \\ -2 \dot{x} + {\varOmega }_y(x, y, z) \\ \dot{z} \\ {\varOmega }_z(x,y,z) \end{array} \right) . \end{aligned}$$

(1)

Here,

$$\begin{aligned} {\varOmega } = {\varOmega }(x,y,z,m_1,m_2,m_3) \frac{1}{2}(x^{2}+y^{2})+\frac{m_{1}}{r_{1}} + \frac{m_{2}}{r_{2}} + \frac{m_{3}}{r_{3}} \end{aligned}$$

is the effective potential, where $r_{i} \sqrt{(x-x_{i})^{2}+(y-y_{i})^{2}+z^2}$, for $i=1,2,3$. The general expressions for the coordinates of the primaries in terms of the masses of the three point masses are given by

$$\begin{aligned} x_1&\frac{-|K| \sqrt{m_2^2 + m_2 m_3 + m_3^2}}{K}, \quad y_1 \mathop {=}\limits ^{\mathrm{def}}0, \\ x_2&\frac{|K|\left[ (m_2 - m_3) m_3 + m_1 (2 m_2 + m_3) \right] }{ 2 K \sqrt{m_2^2 + m_2 m_3 + m_3^2} }, \quad y_2 \mathop {=}\limits ^{\mathrm{def}}\frac{-\sqrt{3} m_3}{2 m_2^{3/2}} \sqrt{\frac{m_2^3}{m_2^2 + m_2 m_3 + m_3^2}}, \\ x_3&\frac{|K|}{2 \sqrt{m_2^2 + m_2 m_3 + m_3^2}}, \quad y_3 \mathop {=}\limits ^{\mathrm{def}}\frac{\sqrt{3}}{2 \sqrt{m_2}} \sqrt{\frac{m_2^3}{m_2^2 + m_2 m_3 + m_3^2}}, \end{aligned}$$

where $K m_{2}(m_{3}-m_{2})+m_{1}(m_{2}+2m_{3})$ and the masses are normalized so that

$$\begin{aligned} m_{1}+m_{2}+m_{3}=1. \end{aligned}$$

We write

$$\begin{aligned} p_1 = (x_1, y_1), \quad \quad p_2 = (x_2, y_2), \quad \quad \text {and} \quad \quad p_3 = (x_3, y_3) \end{aligned}$$

to denote the locations in the plane of the primary bodies.

The equations of motion have the well-known first integral (the so-called Jacobi constant) given by

$$\begin{aligned} C=-(\dot{x}^2+\dot{y}^2+\dot{z}^2)+2{\varOmega }. \end{aligned}$$

The constant C is related to the total energy of the system by means of the relation $E=-C/2$. It should be noted that when $m_{3}=0$ and $m_{2}\mu$ we recover the coordinates of the restricted three-body problem:

$$\begin{aligned} \begin{aligned} (x_{1},y_{1},z_{1})&=(-\mu ,0,0),\\(x_{2},y_{2},z_{2})&=(1-\mu ,0,0),\\ (x_{3},y_{3},z_{3})&=(1/2-\mu ,\sqrt{3}/2,0), \end{aligned} \end{aligned}$$

where the position of the ‘phantom’ mass $m_{3}$ coincides with the equilibrium point $L_{4}$ of the R3BP associated with the masses $m_1$ and $m_2$.

Fig. 4

The circular restricted four-body problem: The primaries with masses $0 < m_3 \le m_2 \le m_1$ move in a central equilateral triangle configuration of Lagrange. After changing to a corotating coordinate frame, we study the dynamics of a fourth and massless particle moving in the gravitational field of the primaries. The equations of motion for the massless particle are given in Eq. (1). For typical mass ratios, the problem has always 8, 9, or 10 relative equilibria (or libration points) depending on the mass ratio. The relative equilibria are denoted here by ${\mathcal {L}}_j$ for $0 \le j \le 9$

The relative equilibria—or libration points—of the system are given by the critical points of the effective potential ${\varOmega }$. That is, they satisfy the equations ${\varOmega }_{x}=0$, ${\varOmega }_{y}=0$, and ${\varOmega }_{z}=0$. A straightforward computation shows that the partial derivative ${\varOmega }_{z}$ satisfies

$$\begin{aligned} {\varOmega }_{z}=-z\sum _{i=1}^{3}\frac{m_{i}}{r_{i}^3}, \end{aligned}$$

with $r_{i}=\sqrt{(x-x_{i})^{2}+(y-y_{i})^{2}+z^2}$ for $i=1,2,3$, and as a consequence, all equilibria are coplanar (i.e., ${\varOmega }_{z}=0$ implies that $z=0$). As mentioned in “Introduction,” there are 8, 9, or 10 equilibria depending on the mass ratios (Fig. 4).

It is not difficult to see that when we have two equal masses, say $m_2=m_3$, the partial derivatives of the effective potential for the planar case satisfy the following properties

$$\begin{aligned} {\varOmega }_{x}(x,-y)&= {\varOmega }_{x}(x,y),\\ {\varOmega }_{y}(x,-y)&=- {\varOmega }_{x}(x,y). \end{aligned}$$

As a consequence, the equations of motion (1) are invariant under the transformations $x \rightarrow x$, $y \rightarrow -y$, $\dot{x} \rightarrow -\dot{x}$, $\dot{y} \rightarrow \dot{y}$, $\ddot{x} \rightarrow \ddot{x}$, $\ddot{y} \rightarrow -\ddot{y}$; therefore, we have recovered the well-known symmetry with respect to the x-axis for the restricted three-body problem. However, for the equal masses case we have an additional and useful symmetry which states that if $z(t)=x(t)+\textit{i}y(t)$ is a solution of the system (in complex notation), then $e^{\frac{2\pi }{3}{} \textit{i}}z(t)$ is also a solution of the system. In other words, we have a symmetry with respect to the lines that join the center of the triangle with the three primaries, see Burgos-García (2013) for further details. A useful consequence of this symmetry with respect to the local dynamics around the equilibrium points is that it is enough to study the equilibrium points on the x-axis. This information is extended to the remaining equilibrium points by means of this symmetry. Moreover, as this property can be applied to study the periodic orbits around the primaries, it is enough to study the dynamics around the primary on the x-axis.

2.2 Overview of methods and results

When searching for spatial periodic orbits in Hamiltonian systems, a natural starting point is the so-called vertical Lyapunov families. These are one-parameter families of spatial periodic orbits near a libration point of saddle $\times$ saddle $\times$ center or saddle $\times$ center $\times$ center stability. For these, we compute a high-order approximation of the center manifold using the approach of Farrés and Jorba (2010). The resulting formal expansion for the center manifold provides good starting points for the vertical Lyapunov families. We then apply a classical numerical continuation scheme for systems with a first integral (e.g., see Keller 1987). Since our continuation approach is based on Newton’s method, we must have local isolation of the solutions. Again, since we are working with a Hamiltonian system, we must introduce both the standard Poincaré condition and an unfolding parameter as discussed in Muñoz Almaraz et al. (2003) to remove the degeneracies caused by the phase and the conservation of energy. We apply our method of proof to some of the orbits located using the continuation scheme.

Another mechanism giving rise to spatial periodic orbits is discussed in the work of Hénon (1973) and starts by considering a planar family of periodic orbits. He shows that computing the so-called vertical stability index (denoted as $a_{v}$) of a planar periodic orbit provides information about whether a planar periodic orbit belongs at the same time to a family of 3D (spatial) periodic orbits. The conclusions of that work suggest that the so-called vertical critical orbits, when $\vert a_{v}\vert =1$, can be considered as members of 3D families of periodic orbits. When we find planar Lyapunov orbits for which $\vert a_{v}\vert =1$, we will find spatial families of periodic orbits after the bifurcation. This mechanism produces the so-called halo and axial orbits families (as well as others). Once again numerical continuation can be applied to any such orbit, and we apply our method of proof to some periodic orbits located this way.

We now outline the main idea behind the computer-assisted proofs carried in the present work. Let ${\varOmega } \subset {\mathbb {R}}^N$ be an open set and $f :{\varOmega } \rightarrow {\mathbb {R}}^N$ be a real analytic vector field. The main objects of study in this paper are periodic solutions of the differential equation ${\dot{{{\mathbf {x}}}}} = f({{\mathbf {x}}})$, that is solutions ${{\mathbf {x}}}:[0, T] \rightarrow {\mathbb {R}}^N$ with ${{\mathbf {x}}}(t+T)={{\mathbf {x}}}(t)$ for all $t \in {\mathbb {R}}$. Following closely the approach of Van den Berg and Sheombarsing (2016), we expand the solution in the basis of Chebyshev series on multiple time domains, and we solve for the Chebyshev coefficients. We endow the space of unknown coefficients with a Banach space structure and are left with the problem of finding a zero of a smooth nonlinear map between Banach spaces. Truncating to a finite number of modes, we compute an approximate solution using Newton’s method. Finally, we make a posteriori arguments which allow us to conclude that there is a true solution of the problem near our numerical approximation. The a posteriori analysis used in the present work follows the approach developed in Hungria et al. (2016) and Van den Berg and Sheombarsing (2016).

Using the methods sketched above, we are able to prove the existence of a number of in- and out-of-plane periodic orbits for the CRFBP.

Remark 2

(Automatic differentiation) The analysis outlined above is based on formal series manipulations and is especially straightforward when the vector field f is polynomial. However, in the present work we consider the CRFBP, whose nonlinearities involve rational denominators originating from the inverse square law of universal gravitation. To circumvent this difficulty, our approach builds on the techniques of automatic differentiation for Fourier series developed in Lessard et al. (2016), and we convert the four-body vector field into a polynomial system—albeit in a higher-dimensional phase space. The idea, which we discuss in details in Sect. 3, is to append additional polynomial differential equations related to the rational nonlinearities. By carefully adding new variables (sometimes called unfolding parameters) to the system (which balance certain scalar constraint equations), we obtain a system of polynomial equations which is equivalent to the original system, in the sense that periodic solutions of one are periodic solutions of the other. We note that in Lessard et al. (2016) additional variable was avoided by exploiting the symmetries of the restricted three-body problem.

2.3 Computer-assisted proofs in Celestial Mechanics

In this section, we provide a brief overview of the literature on computational proofs for N-body problems, with a particular emphasis on results pertaining to periodic solutions. A general review of the literature on computer-assisted proofs in analysis is beyond the scope of the present work, and the interested reader will find extensive scholarly discussion in the book of Tucker (2011), the memoire Eckmann et al. (1984), and also the review articles van den Berg and Lessard (2015) and Koch et al. (1996). The reader is warned also that the discussion below follows a kind of dynamical progression, and is not at all in chronological order.

Regular motions include equilibrium, periodic, and quasiperiodic solutions of the equations of motion. It is sometimes possible to study equilibrium solutions and their stability “by hand” (or with the aid of computer algebra systems); however, it is hard work describing the nonlinear stability—that is following invariant manifolds. We refer to the mathematically rigorous, computer-assisted studies of center manifolds (Capiński and Roldán 2012) and strong stable/unstable manifolds (Capiński and Wasieczko-Zajac 2015) for the circular restricted three-body problem, as well as to the work of Kepley and Mireles James (2018) on the dynamics of complex saddles in the CRFBP.

Techniques for computer-assisted proofs of periodic orbits for differential equations in general, and for celestial mechanics problems in particular, have been developed by a number of authors. See, for example, the studies of Arioli (2004), Arioli et al. (2006), and Lessard et al. (2016) on periodic orbits for the three-body and the planar restricted three-body problem, as well as the computer-assisted proof of the existence of choreography orbits for N-bodies with $3 \le N \le 8$ Kapela and Zgliczyński (2003). The present work provides computer-assisted proofs of spatial orbits in the circular restricted four-body problem. The recent work of Walawska and Wilczak (2018) follows global branches of spatial periodic orbits in the restricted three-body problems, providing mathematically rigorous computer-assisted analysis of the bifurcations.

Computer-assisted proofs of invariant tori in realistic celestial systems are both difficult and technical and can be found in the work of Celletti and Chierchia (1997, 2007). These studies build on the earlier work of Celletti and Chierchia (1987), Celletti et al. (1987), de la Llave and Rana (1990), and Celletti and Chierchia (1991) on the use of the digital computer as a tool for optimizing KAM estimates. See also the recent work of Haro and de la Llave (2006) on a general approach to computer-assisted proofs for invariant tori. Note that in the studies just mentioned, the invariant tori are constructed explicitly via Fourier series approximation. Another, more existential approach to KAM theorem is found in the work of Kapela and Simó (2017), where the authors use methods of rigorous numerical integration in order to compute normal forms about periodic orbits of Hamiltonian systems and check the conditions of abstract stability theorems. Using these techniques, they show, for example, that the rotating figure-eight choreography orbit in the full three-body problem is KAM stable.

We refer also to the work of Galante and Kaloshin (2011) on the destruction of invariant tori in the planar circular restricted three-body problem and the study of Urschel and Galante (2013) on diffusion in a Sun–Jupiter–Asteroid problem.

The study of irregular motions often focuses on transverse homoclinic/heteroclinic chaos or on the existence of topological horseshoes. See, for example, the studies of Arioli (2002), Wilczak and Zgliczynski (2003), and Wilczak and Zgliczyński (2005) on connecting orbits and chaos between periodic orbits in the circular restricted three-body problem. See also the work of Capiński (2012) on transverse intersection between the stable/unstable manifold of such orbits. The recent work of Kepley and Mireles James (2018) establishes the existence of transverse homoclinic orbits, and hence chaotic motions, for a saddle-focus equilibrium in the CRFBP.

2.4 A posteriori existence and computer-assisted proof in nonlinear analysis

We now state a theorem which provides sufficient conditions for the existence of a zero to a nonlinear equation, provided one has a good enough, non-degenerate approximate solution. The theorem makes precise the meaning of the terms “good enough” and “non-degenerate” and provides computable conditions for checking these conditions. The reader will find similar theorems with their proofs in the references Hungria et al. (2016), Eckmann et al. (1984), Gameiro and Lessard (2017), Day et al. (2007), Yamamoto (1998), and Arioli and Koch (2012).

Theorem 1

(Radii polynomial approach) Let X and Y be Banach spaces, $F :X \rightarrow Y$ be a twice Fréchet differentiable mapping and ${{\bar{x}}} \in X$ (typically a numerical approximation). Denote by $\Vert \cdot \Vert _X$ the norm on X, $\overline{B_r({\bar{x}})} = \{x \in X : \Vert x-{\bar{x}}\Vert \le r\}$ the closed ball centered at ${\bar{x}}$, and $\Vert \cdot \Vert _{B(X)}$ the bounded linear operator norm. Suppose that $A^\dagger :X \rightarrow Y$ and $A :Y \rightarrow X$ are bounded linear operators and that A is one-to-one (injective). Assume that there are constants $Y_0, Z_0, Z_1 \ge 0$ and a positive function $Z_2 :(0, \infty ) \rightarrow (0, \infty )$ having that

$$\begin{aligned} \Vert A F(x) \Vert _{X}&\le Y_0, \end{aligned}$$

(2)

$$\begin{aligned} \Vert \text{ Id }_X - A A^\dagger \Vert _{B(X)}&\le Z_0, \end{aligned}$$

(3)

$$\begin{aligned} \Vert A \left( DF({\bar{x}}) - A^\dagger \right) \Vert _{B(X)}&\le Z_1, \end{aligned}$$

(4)

$$\begin{aligned} \Vert A \left( DF(x) - DF({\bar{x}}) \right) \Vert _{B(X)}&\le Z_2(r) r, \qquad \text{ for } x \in \overline{B_r({\bar{x}})}. \end{aligned}$$

(5)

Define the function

$$\begin{aligned} p(r) Z_2(r) r^2 - (1 - Z_0 ) r + Y_0. \end{aligned}$$

(6)

If there exists an $r_0 > 0$ so that $p(r_0) < 0$, then there exists a unique ${\tilde{x}}\in B_r({\bar{x}})$ such that $F({\tilde{x}}) = 0$.

Remark 3

In many applications, the function $Z_2(r)$ is a polynomial in r. In this case, p(r) is a polynomial which we refer to as the radii polynomial. This happens in particular when F is a polynomial map on a product of Banach algebras, the case considered in the present work.

3 Automatic differentiation for the CRFBP: the equivalent polynomial system

In this section, we derive a nine-dimensional polynomial vector field and show that periodic solutions of the new problem correspond to periodic solutions of the six-dimensional CRFBP. The polynomial vector field is obtained by automatic differentiation, a process by which we add algebraic differential equations to our system whose solutions correspond to the original non-polynomial nonlinearity.

The idea of replacing a given nonlinear system of differential equation with a polynomial vector field is not new. Examples of using this idea to simplify the development of Taylor integration schemes for celestial mechanics problems appear in the literature as early as the works of Steffensen (1955), Rabe (1961), and Deprit and Price (1965). In the context of computer-assisted proofs, it is important to describe precisely the relationship between the original and the polynomial problems. (The problems are not strictly speaking equivalent; for example, in addition to being of different dimensions the polynomial problem is entire and the later has singularities at the locations of the primaries.) The study of Kepley and Mireles James (2018) presents a dynamical systems approach to justifying the automatic differentiation, which we recapitulate below.

3.1 The infinitesimal conjugacy equation

Let $U \subset {\mathbb {R}}^M$ be an open subset and $f :U \rightarrow {\mathbb {R}}^M$ be a smooth non-polynomial vector field. We look for a transformation h which embeds the vector field in a polynomial system. Let us denote the polynomial vector field by g. We want that the dynamics of the polynomial vector field, when restricted to a certain submanifold, are conjugated to the original dynamics generated by f.

To be more precise, we seek an $N > 0$, a smooth function $h :U \subset {\mathbb {R}}^M \rightarrow {\mathbb {R}}^N$, and a polynomial vector field $g :{\mathbb {R}}^{M+N} \rightarrow {\mathbb {R}}^{M+N}$ with

$$\begin{aligned} \left( \begin{array}{c} f({{\mathbf {x}}}) \\ Dh({{\mathbf {x}}}) f({{\mathbf {x}}}) \end{array} \right) = g({{\mathbf {x}}}, h({{\mathbf {x}}})), \qquad \quad {{\mathbf {x}}}\in U. \end{aligned}$$

(7)

Defining $R :U \rightarrow {\mathbb {R}}^{M+N}$ by

$$\begin{aligned} R({{\mathbf {x}}}) = \left( \begin{array}{c} {{\mathbf {x}}}\\ h({{\mathbf {x}}}) \end{array} \right) , \end{aligned}$$

we see that Eq. (7) is equivalent to the infinitesimal conjugacy equation

$$\begin{aligned} DR({{\mathbf {x}}}) f({{\mathbf {x}}}) = g(R({{\mathbf {x}}})), \end{aligned}$$

(8)

for ${{\mathbf {x}}}\in U \subset {\mathbb {R}}^M$. The dynamical interpretation of Eq. (8) is that the vector field g restricted to the graph of h is equivalent to the vector field f pushed forward by R, so that orbits of g on the graph of h correspond to orbits of f. Indeed, the following Lemma is proven in Kepley and Mireles James (2018).

Lemma 1

Suppose that f, g, R are as above.

• Then, the image of R, that is, the graph of h, is an invariant manifold for the flow generated by g.

• Let $\pi _M :{\mathbb {R}}^{M+N} \rightarrow {\mathbb {R}}^M$ denote projection onto the first M components. Then, if $u :[0, T] \rightarrow {\mathbb {R}}^{M+N}$ is a solution of the differential equation $\dot{u} = g(u)$, we have that

  $$\begin{aligned} {{\mathbf {x}}}(t) \pi _M(u(t)) \end{aligned}$$

  is a solution of the differential equation ${\dot{{{\mathbf {x}}}}} = f({{\mathbf {x}}})$ with initial conditions $\pi _M(u(0))$.

In a particular problem involving a non-polynomial vector field f, the challenge is to find g and h. The procedure for this is straightforward when f contains N non-polynomial terms which are themselves solutions of polynomial ordinary differential equations. This procedure is best illustrated by considering particular examples. We note that this approach to automatic differentiation of vector fields is a generalization of the approach developed for Taylor series more commonly discussed in the literature (as, for example, in Jorba and Zou 2005; Knuth 1981; Haro et al. 2016). This approach has the virtue of applying also to the basis such as Fourier and Chebyshev as well as Taylor series. See Lessard et al. (2016), van den Berg et al. (2018), and the discussion below.

3.2 Automatic differentiation for the CRFBP

Returning to the equations of motion for the CRFBP defined in Sect. 2.1, we define variables

$$\begin{aligned} u_1 x, \quad u_2 \mathop {=}\limits ^{\mathrm{def}}\dot{x} , \quad u_3 \mathop {=}\limits ^{\mathrm{def}}y, \quad u_4 \mathop {=}\limits ^{\mathrm{def}}\dot{y}, \quad u_5 \mathop {=}\limits ^{\mathrm{def}}z, \quad u_6 \mathop {=}\limits ^{\mathrm{def}}\dot{z}, \end{aligned}$$

and

$$\begin{aligned} u_7 \frac{1}{r_1}, \quad u_8 \mathop {=}\limits ^{\mathrm{def}}\frac{1}{r_2}, \quad \text {and} \quad u_9 \mathop {=}\limits ^{\mathrm{def}}\frac{1}{r_3}, \end{aligned}$$

where

$$\begin{aligned} r_1&= \sqrt{(x-x_1)^2 + (y-y_1)^2 + z^2}, \\ r_2&= \sqrt{(x-x_2)^2 + (y-y_2)^2 + z^2}, \\ r_3&= \sqrt{(x-x_3)^2 + (y-y_3)^2 + z^2}. \end{aligned}$$

Recall that $(x_j, y_j)$ for $j = 1,2,3$ are the coordinates of the three primary bodies. The virtue of these variables is seen by observing that

$$\begin{aligned} {\varOmega }_x&= x - \frac{m_1(x - x_1)}{r_1^3} - \frac{m_2(x - x_2)}{r_2^3} - \frac{m_3(x - x_3)}{r_3^3} \\&= u_1 - m_1(u_1 - x_1) u_7^3 - m_2(u_1 - x_2) u_8^3 - m_3(u_1 - x_3)u_9^3, \\ {\varOmega }_y&= y - \frac{m_1(y - y_1)}{r_1^3} - \frac{m_2(y - y_2)}{r_2^3} - \frac{m_3(y - y_3)}{r_3^3} \\&= u_3 - m_1(u_3 - y_1) u_7^3 - m_2( u_3 - y_2) u_8^3 - m_3(u_3 - y_3)u_9^3, \\ {\varOmega }_z&= - \frac{m_1z }{r_1^3} - \frac{m_2 z }{r_2^3} - \frac{m_3 z}{r_3^3} \\&= - m_1 u_5 u_7^3 - m_2 u_5 u_8^3 - m_3 u_5 u_8^3. \end{aligned}$$

That is, the CRFBP nonlinearities are polynomial in the new variables.

To understand the dynamics in terms of these new variables, consider, for example, that

$$\begin{aligned} \dot{u}_7&= \frac{-1}{r_1^2} \dot{r}_1 \\&= \frac{-1}{r_1^2}\frac{\mathrm{d}}{\mathrm{d}t} \sqrt{(x(t)-x_1)^2 + (y(t) - y_1)^2 + z(t)^2} \\&= \frac{-1}{r_1^2} \frac{\frac{\mathrm{d}}{\mathrm{d}t}(x(t)-x_1)^2 + (y(t) - y_1)^2 + z(t)^2}{2\sqrt{(x(t)-x_1)^2 + (y(t) - y_1)^2 + z(t)^2}} \\&= - (u_1 - x_1)u_2 u_7^3 - (u_3 - y_1)u_4 u_7^3 - u_5 u_6 u_7^3, \end{aligned}$$

and similarly that

$$\begin{aligned} \dot{u}_8&= - (u_1 -x_2) u_2 u_8^3 - (u_3-y_2) u_4 u_8^3 - u_5 u_6 u_8^3, \\ \dot{u}_9&= - (u_1-x_3) u_2 u_9^3 - (u_3-y_3) u_4 u_9^3 - u_5 u_6 u_9^3 . \end{aligned}$$

Based on these considerations, let ${{\mathbf {x}}}(u_1, \dots , u_6) \in {\mathbb {R}}^6$ and define the set

$$\begin{aligned} U = \left\{ {{\mathbf {x}}}= (u_1, \dots , u_6) : u_1 \ne x_j \text { and } u_3 \ne y_j \text { for } j = 1,2,3 \right\} . \end{aligned}$$

Define the smooth function $h :U \subset {\mathbb {R}}^6 \rightarrow {\mathbb {R}}^3$ by

$$\begin{aligned} h({{\mathbf {x}}}) = \begin{pmatrix} \frac{1}{\sqrt{(u_1-x_1)^2 + (u_3-y_1)^2 + u_5^2}} \\ \frac{1}{\sqrt{(u_1-x_2)^2 + (u_3-y_2)^2 + u_5^2}} \\ \frac{1}{\sqrt{(u_1-x_3)^2 + (u_3-y_3)^2 + u_5^2}} \end{pmatrix} \end{aligned}$$

and let $u = (u_1, \dots , u_9) R({{\mathbf {x}}}) = ({{\mathbf {x}}},h({{\mathbf {x}}})) \in {\mathbb {R}}^9$, where $R :U \rightarrow {\mathbb {R}}^9$ is smooth. Finally, let the polynomial vector field $g :{\mathbb {R}}^9 \rightarrow {\mathbb {R}}^9$ given by

$$\begin{aligned} g(u) \begin{pmatrix} u_2 \\ 2u_4 + u_1 - m_1 (u_1-x_1) u_7^3 - m_2 (u_1-x_2) u_8^3 - m_3 (u_1 - x_3) u_9^3 \\ u_4 \\ -2 u_2 + u_3 - m_1 (u_3-y_1) u_7^3 - m_2 (u_3 - y_2) u_8^3 - m_3 (u_3 - y_3) u_9^3 \\ u_6 \\ -m_1 u_5 u_7^3 - m_2 u_5 u_8^3 - m_3 u_5 u_9^3 \\ - (u_1 - x_1)u_2 u_7^3 - (u_3 - y_1)u_4 u_7^3 - u_5 u_6 u_7^3 \\ - (u_1 -x_2) u_2 u_8^3 - (u_3-y_2) u_4 u_8^3 - u_5 u_6 u_8^3 \\ - (u_1-x_3) u_2 u_9^3 - (u_3-y_3) u_4 u_9^3 - u_5 u_6 u_9^3 \end{pmatrix}. \end{aligned}$$

(9)

With g and R so defined it is a straightforward calculation to verify that Eq. (8) is satisfied for the CRFBP field f. Recalling Lemma 1, we have the following result.

Lemma 2

If $u = (u_1,\dots ,u_9) :[0, T] \rightarrow {\mathbb {R}}^9$ is a T-periodic solution of $\dot{u}=g(u)$, then ${{\mathbf {x}}}(t) \pi _6(u(t)) = (u_1,\dots ,u_6) :[0, T] \rightarrow {\mathbb {R}}^6$ is a T-periodic solution of the CRFBP ${\dot{{{\mathbf {x}}}}} = f({{\mathbf {x}}})$ with f given in (1).

3.3 Unfolding parameters

Periodic solutions of the polynomial system defined in Lemma 2 occur in five parameter families and are hence not isolated. The five unit Floquet multipliers come from

• (a) The shift invariance always present when we study periodic solutions of vector fields;

• (b) The fact that g inherits a first integral from f;

• (c) The fact that each of the three appended equations introduces a spurious periodic family. We say that the extra families are spurious as they lie off the image of R and hence have nothing to do with the dynamics of the CRFBP. Nevertheless, they are present when we study g and have to be understood/excluded.

The degeneracy introduced by (a) is handled by introducing a phase condition. We take a standard Poincaré section. The degeneracy introduced by (b) is handled by fixing the desired frequency/period. This choice must be balanced by introducing an unfolding parameter to re-balance the system of equation. This classical technique is discussed, for example, in the works of Muñoz Almaraz et al. (2003), Sepulchre and MacKay (1997) and Muñoz Almaraz et al. (2000). Each degeneracy from (c) is due to the fact that we have to impose that the periodic orbit is on the manifold parameterized by R. We achieve this by introducing three additional scalar constraint equations. Each of these constraint equations must be balanced by its own unfolding parameter, resulting in a total of four. In the end, these parameters will end up being zero, as we show below. Their ultimate purpose is to remove the four-dimensional kernel—resulting from the degeneracies just mentioned—from the linearized problem.

More precisely then, we let $\alpha _1, \alpha _2, \alpha _3, \beta \in {\mathbb {R}}$ the unfolding parameters and consider the augmented system of equations

$$\begin{aligned}&\dot{u}_1 = u_2, \nonumber \\&\dot{u}_2 = 2u_4 + u_1 - m_1 (u_1-x_1) u_7^3 - m_2 (u_1-x_2) u_8^3 - m_3 (u_1 - x_3) u_9^3 + \beta u_2, \nonumber \\&\dot{u}_3 = u_4, \nonumber \\&\dot{u}_4 = -2 u_2 + u_3 - m_1 (u_3-y_1) u_7^3 - m_2 (u_3 - y_2) u_8^3 - m_3 (u_3 - y_3) u_9^3, \nonumber \\&\dot{u}_5 = u_6, \nonumber \\&\dot{u}_6 = -m_1 u_5 u_7^3 - m_2 u_5u_8^3 - m_3 u_5 u_9^3, \nonumber \\&\dot{u}_7 = - (u_1 - x_1)u_2 u_7^3 - (u_3 - y_1)u_4 u_7^3 - u_5 u_6 u_7^3 + \alpha _1 u_7^3, \nonumber \\&\dot{u}_8 = - (u_1 -x_2) u_2 u_8^3 - (u_3-y_2) u_4 u_8^3 - u_5 u_6 u_8^3 + \alpha _2 u_8^3, \nonumber \\&\dot{u}_9 = - (u_1-x_3) u_2 u_9^3 - (u_3-y_3) u_4 u_9^3 - u_5 u_6 u_9^3 + \alpha _3 u_9^3. \end{aligned}$$

(10)

Denote $\alpha =(\alpha _1,\alpha _2,\alpha _3) \in {\mathbb {R}}^3$, and denoting the right-hand side of (10) by ${{\tilde{g}}}(u,\beta ,\alpha )$, we get

$$\begin{aligned} {{\tilde{g}}}(u,\beta ,\alpha ) g(u) + \begin{pmatrix} 0 \\ \beta u_2 \\ 0 \\ 0 \\ 0 \\ 0 \\ \alpha _1 u_7^3 \\ \alpha _2 u_8^3 \\ \alpha _3 u_9^3 \end{pmatrix}. \end{aligned}$$

We have the following lemma, which is related to the results of Muñoz Almaraz et al. (2003). Since the lemma does not exactly follow directly from any of the classical results, we include the proof—which involves some tedious calculations—in “Appendix” for the sake of completeness.

Lemma 3

Assume that $\alpha _1, \alpha _2, \alpha _3, \beta , \omega \in {\mathbb {R}}$ are fixed constants with $\omega > 0$, and let ${\mathbf {n}}, {\mathbf {p}} \in {\mathbb {R}}^9$ be fixed vectors. Let $T = 2 \pi / \omega$. Suppose that $u = (u_1,\dots ,u_9) :[0, T] \rightarrow {\mathbb {R}}^9$ is a T-periodic solution of $\dot{u} = {{\tilde{g}}}(u,\beta ,\alpha )$ with

$$\begin{aligned} 0&= \left( u(0) - {\mathbf {p}} \right) \cdot {\mathbf {n}}, \nonumber \\ u_7(0)&= \frac{1}{\sqrt{(u_1(0) - x_1)^2 + (u_3(0) - y_1)^2 + u_5(0)^2}}, \nonumber \\ u_8(0)&= \frac{1}{\sqrt{(u_1(0) - x_2)^2 + (u_3(0) - y_2)^2 + u_5(0)^2}}, \nonumber \\ u_9(0)&= \frac{1}{\sqrt{(u_1(0) - x_3)^2 + (u_3(0) - y_3)^2 + u_5(0)^2}}, \end{aligned}$$

(11)

and that $u_7(t), u_8(t), u_9(t) > 0$ for all $t \in [0, T]$. Then,

• (i) $\alpha _1 = \alpha _2 = \alpha _3 = \beta = 0$, and

• (ii) the function ${{\mathbf {x}}}(u_1,\dots ,u_6) :[0, T] \rightarrow {\mathbb {R}}^6$ is a T-periodic solution of the circular restricted four-body problem ${\dot{{{\mathbf {x}}}}} = f({{\mathbf {x}}})$ with f given in (1).

4 The rigorous computational approach based on Chebyshev series

Based on the analysis provided by the previous section, we now define a nonlinear Chebyshev operator equation of the form $F(x)=0$ on a Banach space of infinite sequences whose zeros correspond to periodic orbits of $\dot{u} = {{\tilde{g}}}(u,\beta ,\alpha )$, and via Lemma 3 to periodic orbits of the CRFBP. To define the Chebyshev operator, we employ the techniques described in the paper Van den Berg and Sheombarsing (2016), following closely their notation and approach. Once the operator is obtained, we will apply the radii polynomial approach (as described in Theorem 1) to prove existence of solutions of $F(x)=0$.

As in Van den Berg and Sheombarsing (2016), considering any partition of [0, 1]

$$\begin{aligned} {\mathcal {P}}_m \{ t_0=0<t_1<t_2<\cdots<t_{m-1}<t_m =1 \}, \end{aligned}$$

(12)

where $m \in {\mathbb {N}}$ is the mesh size. Fix $\omega > 0$, and let ${\mathbf {n}}, {\mathbf {p}} \in {\mathbb {R}}^9$ be fixed vectors. Looking for periodic orbits of (10) is equivalent to

$$\begin{aligned} ({\mathbf{P}}_1)&\left\{ \begin{array}{lll} \displaystyle \frac{\mathrm{d}}{\mathrm{d}t}u^{(1)}(t) = \frac{1}{\omega } {{\tilde{g}}}(u^{(1)}(t),\beta ,\alpha ), \quad t \in [0,t_1], \\ u^{(1)}(0)=u^{(m)}(1) , \\ (u^{(1)}(0)-{\mathbf {p}}) \cdot {\mathbf {n}} =0, \\ \left( u^{(1)}_7(0)\right) ^2 \left( \left( u^{(1)}_1(0)-x_1\right) ^2+\left( u^{(1)}_3(0)-y_1\right) ^2+\left( u^{(1)}_5(0)\right) ^2 \right) = 1 , \\ \left( u^{(1)}_8(0)\right) ^2 \left( \left( u^{(1)}_1(0)-x_2\right) ^2+\left( u^{(1)}_3(0)-y_2\right) ^2+\left( u^{(1)}_5(0)\right) ^2 \right) = 1, \\ \left( u^{(1)}_9(0)\right) ^2 \left( \left( u^{(1)}_1(0)-x_3\right) ^2+\left( u^{(1)}_3(0)-y_3\right) ^2+\left( u^{(1)}_5(0)\right) ^2 \right) = 1. \end{array} \right. \\ ({\mathbf{P}}_i)&\left\{ \begin{array}{lll} \displaystyle \frac{\mathrm{d}}{\mathrm{d}t} u^{(i)}(t) = \frac{1}{\omega } {\tilde{g}}(u^{(i)}(t),\beta ,\alpha ), \quad t \in [t_{i-1},t_i], \\ u^{(i)}(t_{i-1}) = u^{(i-1)}(t_{i-1}), \end{array} \right. \text { for } i=2,\dots ,m, \end{aligned}$$

where $u^{(i)}:[t_{i-1},t_i] \rightarrow {\mathbb {R}}^n$ is a solution of the differential equation $\dot{u} = \frac{1}{\omega } {\tilde{g}}(u,\beta ,\alpha )$ on the time interval $[t_{i-1},t_i]$ for $i=1,2,\dots ,m$. The idea of the approach is to solve each problem (${\mathbf{P}}_i$) on the time interval $[t_{i-1},t_i]$ for each $i=1,2,\dots ,m$ using Chebyshev series expansions of each component $u_k^{(i)}$ ($k=1,\dots ,9$) of the solutions. As we shall see, solving simultaneously all problems (${\mathbf{P}}_1$), ..., (${\mathbf{P}}_m$) using Chebyshev series will lead to the equivalent zero finding problem $F(x)=0$ posed on a Banach space of infinite sequences of Chebyshev coefficients.

For each time subdomain index $i=1,\dots ,m$, let $\sigma _i:[-1,1] \rightarrow [t_{i-1},t_i]$ be given by

$$\begin{aligned} \sigma _i(t) \frac{t_i-t_{i-1}}{2}(t+1) + t_{i-1}, \end{aligned}$$

(13)

and let ${\tilde{u}}^{(i)}: [-1,1] \rightarrow {\mathbb {R}}^9$ be given by ${\tilde{u}}^{(i)}(t) u^{(i)}(\sigma _i(t))$. Hence, if $u^{(i)}$ is a solution of the differential equation $\dot{u} = \frac{1}{\omega } {\tilde{g}}(u,\beta ,\alpha )$ on the time interval $[t_{i-1},t_i]$, then ${\tilde{u}}^{(i)}$ is a solution of the differential equation $\dot{u} = \frac{t_i-t_{i-1}}{2 \omega } {\tilde{g}}(u,\beta ,\alpha )$ on the time interval $[-1,1]$. Given any $i \in \{ 1,\dots ,m\}$ and $j \in \{ 1,\dots ,9\}$, expand ${\tilde{u}}_j^{(i)}: [-1,1] \rightarrow {\mathbb {R}}$ in Chebyshev series as

$$\begin{aligned} {\tilde{u}}_j^{(i)}(t) = \left[ a^{(i)}_j\right] _0 + 2 \sum _{k=1}^{\infty } \left[ a^{(i)}_j\right] _k T_k(t), \qquad t \in [-1,1], \end{aligned}$$

(14)

and denote $a^{(i)}_j = \left( [a^{(i)}_j]_k \right) _{k \ge 0}$ the infinite sequence of Chebyshev coefficients of ${\tilde{u}}_j^{(i)}$. Moreover, given $i \in \{ 1,\dots ,m\}$ denote $a^{(i)} = \left( a^{(i)}_1,a^{(i)}_2,\dots ,a^{(i)}_9 \right)$, the vector containing the infinite sequences of Chebyshev coefficients of each of the nine components of the solution ${\tilde{u}}^{(i)}: [-1,1] \rightarrow {\mathbb {R}}^9$.

Given a number $\rho \ge 0$ and a sequence of real numbers $c=(c_k)_{k \ge 0}$, define the weighted $\ell ^1$ norm

$$\begin{aligned} \Vert c\Vert _{(\rho ,1)} |c_0| + 2 \sum _{k =1}^\infty |c_k| \rho ^k. \end{aligned}$$

Given $n \in {\mathbb {N}}$, define the sequence space

$$\begin{aligned} \ell _{(\rho ,n)}^1 \left\{ a = (a_1,a_2,\dots ,a_n) ~\Big |~ a_j = \left( [a_j]_k \right) _{k \ge 0} \text { and } \Vert a_j\Vert _{(\rho ,1)} < \infty , ~ 1 \le j \le n \right\} . \end{aligned}$$

The sequence space $\ell _{(\rho ,n)}^1$ is endowed with the norm

$$\begin{aligned} \Vert a \Vert _{(\rho ,n)} \max _{j=1,\dots ,n} \left\{ \Vert a_j\Vert _{(\rho ,1)} = |[a_j]_0| + 2 \sum _{k =1}^\infty |[a_j]_k| \rho ^k \right\} . \end{aligned}$$

Given a sequence of decay rates $\nu = (\nu _i)_{i=1}^m \in {\mathbb {R}}^m_+$, denote the Banach space

$$\begin{aligned} X_\nu {\mathbb {R}}^4 \times \prod _{i=1}^m \ell _{(\nu _i,n)}^1. \end{aligned}$$

The norm $\Vert \cdot \Vert _{X_\nu }$ on the space $X_\nu$ is defined as follows. Given

$$\begin{aligned} x = (\beta ,\alpha ,a^{(1)},\dots ,a^{(m)}) \in {\mathbb {R}}^4 \times \prod _{i=1}^m \ell _{(\nu _i,n)}^1 = X_\nu , \end{aligned}$$

its norm is given by

$$\begin{aligned} \Vert x \Vert _{X_\nu } = \max \left\{ |\beta |, | \alpha _1 |, | \alpha _2 | ,| \alpha _3 |, \Vert a^{(1)}\Vert _{(\nu _1,n)} , \Vert a^{(2)}\Vert _{(\nu _2,n)} , \dots , \Vert a^{(m)}\Vert _{(\nu _m,n)} \right\} . \end{aligned}$$

Definition 1

(Chebyshev operator for periodic orbits) Let $\nu =(\nu _i)_{i=1}^m$ and ${\tilde{\nu }}=({\tilde{\nu }}_i)_{i=1}^m$ be some weights with $1<{\tilde{\nu }}_i<\nu _i$ for all $i=1,\dots ,m$. Fix $\omega >0$ and two vectors ${\mathbf {n}}, {\mathbf {p}} \in {\mathbb {R}}^9$. The Chebyshev operator for periodic orbits is the mapping $F: X_\nu \rightarrow X_{{\tilde{\nu }}}$ defined by

$$\begin{aligned} F(x) = \left( F_0(a^{(1)}), F_1(\beta ,\alpha ,a^{(m)},a^{(1)}), F_2(\beta ,\alpha ,a^{(1)},a^{(2)}),\dots , F_m(\beta ,\alpha ,a^{(m-1)},a^{(m)}) \right) , \end{aligned}$$

where $F_0:\ell _{(\nu _1,n)}^1 \rightarrow {\mathbb {R}}^4$ and $F_i:{\mathbb {R}}^4 \times \ell _{(\nu _{i-1},n)}^1 \times \ell _{(\nu _{i},n)}^1 \rightarrow \ell _{({\tilde{\nu }}_i,n)}^1$ are given by

$$\begin{aligned} F_0(a^{(1)})&\left\{ \begin{array}{l} \displaystyle \sum _{j=1}^9 \left( \left[ a^{(1)}_j\right] _0 + 2 \sum _{k=1}^{N-1} (-1)^k \left[ a^{(1)}_j\right] _k - {\mathbf {p}}_j \right) {\mathbf {n}}_j \\ \left( u^{(1)}_7(0)\right) ^2 \left( \left( u^{(1)}_1(0)-x_1\right) ^2+\left( u^{(1)}_3(0)-y_1)^2+(u^{(1)}_5(0)\right) ^2 \right) -1 \\ \left( u^{(1)}_8(0)\right) ^2 \left( \left( u^{(1)}_1(0)-x_2\right) ^2+\left( u^{(1)}_3(0)-y_2\right) ^2+\left( u^{(1)}_5(0)\right) ^2 \right) - 1 \\ \left( u^{(1)}_9(0)\right) ^2 \left( \left( u^{(1)}_1(0)-x_3\right) ^2+\left( u^{(1)}_3(0)-y_3\right) ^2+\left( u^{(1)}_5(0)\right) ^2 \right) - 1 \end{array}, \right. \end{aligned}$$

where for $j=1,3,5,7,8,9$, the $u^{(1)}_j(0) [a_j^{(1)}]_0 + 2 \sum _{k \ge 1} (-1)^k [a_j^{(1)}]_k$, and where for $i=1,\dots ,m$

$$\begin{aligned} F_i(\beta ,\alpha ,a^{(i-1)},a^{(i)})&\left\{ \begin{array}{l} \displaystyle [a^{(i)}]_0 - [a^{(i-1)}]_0 + 2 \sum _{k=1}^\infty \left( (-1)^k [a^{(i)}]_k - [a^{(i-1)}]_k \right) , \quad k=0 \\ \displaystyle \omega k [a^{(i)}]_k - \frac{t_i-t_{i-1}}{4} \left( [\phi ^{(i)}]_{k-1} - [\phi ^{(i)}]_{k+1} \right) , \quad k \ge 1, \end{array} \right. \end{aligned}$$

where we set $a^{(0)}=a^{(m)}$, and where $\phi ^{(i)}=\phi ^{(i)}(\beta ,\alpha ,a^{(i)})$ represents the Chebyshev coefficients of ${\tilde{g}}(u^{(i)},\beta ,\alpha )$, that is for $j=1,\dots ,9$

$$\begin{aligned} {\tilde{g}}_j(u^{(i)}(t),\beta ,\alpha ) = [\phi _j^{(i)}]_0 + 2 \sum _{k=1}^\infty [\phi _j^{(i)}]_k T_k(t), \qquad t \in [-1,1]. \end{aligned}$$

Lemma 4

Fix $\omega >0$, ${\mathbf {p}}, {\mathbf {n}} \in {\mathbb {R}}^9$, $m \in {\mathbb {N}}$ and a partition ${\mathcal {P}}_m$ of [0, 1] as in (12). Let $T 1/\omega$. Consider the Chebyshev operator as defined in Definition 1. Let $\nu =(\nu _i)_{i=1}^m$ and assume that $x = (\beta ,\alpha ,a^{(1)},\dots ,a^{(m)}) \in X_\nu$ satisfies $F(x)=0$. For each $i=1,\dots ,m$, define ${\tilde{u}}^{(i)}:[-1,1] \rightarrow {\mathbb {R}}^9$ component-wise by (14). Recall (13) and define $u:[0,T] \rightarrow {\mathbb {R}}^9$ component-wise (that is for $j=1,\dots ,9$) by

$$\begin{aligned} u_j(t) {\tilde{u}}_j^{(i)} (\sigma _i(t/T)), \quad \text {if } t/T \in [t_{i-1},t_i] \subset [0,1]. \end{aligned}$$

Then, $u:[0,T] \rightarrow {\mathbb {R}}^9$ is a T-periodic solution of $\dot{u} = {\tilde{g}}(u,\beta ,\alpha )$ satisfying the four conditions (11). Moreover, ${{\mathbf {x}}}(t) \pi _6(u(t)) = (u_1,\dots ,u_6) :[0, T] \rightarrow {\mathbb {R}}^6$ is a T-periodic solution of the CRFBP ${\dot{{{\mathbf {x}}}}} = f({{\mathbf {x}}})$ with f given in (1).

Based on the analysis of Lemma 4, a vector $x \in X_\nu$ satisfying $F(x)=0$ defines a periodic orbit in the CRFBP. Finally, obtaining computer-assisted proofs of existence of periodic orbits in the CRFBP boils down to applying the radii polynomial approach (as presented in Theorem 1) to compute rigorously solutions of $F=0$. To apply Theorem 1, we need the following ingredients: a numerical approximation ${\bar{x}}$, an approximate derivative $A^\dagger$ of $DF({\bar{x}})$, an approximate inverse A of $DF({\bar{x}})$, and the bounds $Y_0$, $Z_0$, $Z_1$, and $Z_2$ satisfying, respectively (2)–(5). The construction of these ingredients is standard in the field of rigorous numerics in dynamics, and we refer to the paper Van den Berg and Sheombarsing (2016) for their explicit derivation. Perhaps, the only difference with the approach of Van den Berg and Sheombarsing (2016) is the way we compute the discrete convolutions involved in the components of the Chebyshev operator F. The next remark provides details about this.

Remark 4

(Controlling the numerical instability of weighted $\ell ^1$ norms) To define $Y_0$ satisfying (2), we must compute rigorously an upper bound for $\Vert A F({\bar{x}})\Vert _{X_\nu }$. This computation involves controlling weighted $\ell ^1$ norms of the terms $\phi ^{(i)} = \left( [\phi ^{(i)}]_k \right) _{k \ge 0}$ in the definition of $F_i$. Since the terms in $\phi ^{(i)}$ are defined by cubic, quartic, and quintic convolutions, the computation of their weighted $\ell ^1$ norms can be unstable numerically, especially when the vector of decay rates $\nu \in {\mathbb {R}}_+^m$ has large components (which is often necessary to show that the bound $Z_1$ satisfying in (4) is such that $Z_1<1$—a necessary condition for the radii polynomial approach to succeed). To control this numerical instability, we used the method introduced in Lessard (2018) (which combines the FFT algorithm and the property that the sequence space $\ell _{(\rho ,1)}^1$ is a Banach algebra under discrete convolutions) to compute rigorous enclosure of discrete convolutions which decay exponentially fast. This approach stabilizes the computation of the norms in $\ell _{(\rho ,1)}^1$ of the components of the Chebyshev operator F.

We are now ready to present several computer-assisted proofs of existence of periodic orbits in the CRFBP.

5 Results

Using the interval arithmetic MATLAB package INTLAB (Rump 1999), we wrote a computer program implementing a rigorous implementation of the bounds $Y_0$, $Z_0$, $Z_1$, and $Z_2$ satisfying (2)–(5), respectively. For a selection of numerical approximations ${\bar{x}}$ obtained using our continuation scheme, we proved the existence of $r>0$ such that the radii polynomial p defined in (6) satisfy $p(r)<0$. The number r is the radius of the closed ball about ${\bar{x}}$ $\overline{B_{r}({\bar{x}})} \subset X_\nu$, which contains a unique solution ${\tilde{x}}$ of the Chebyshev operator equation $F(x)=0$. Moreover, the radius r provides a $C^0$ error between the numerical approximation ${\bar{u}}:[0,T] \rightarrow {\mathbb {R}}^9$ and the true periodic solution ${\tilde{u}}:[0,T] \rightarrow {\mathbb {R}}^9$.

For each family, we provide the initial positions and velocities. For sake of simplicity of the presentation, in all but one case, we show only four digits after the decimal point (see Tables 1, 2, 3, 4, 7, 8), even though for the computer-assisted proofs, the numerical approximations have a 16-decimal representation. For the halo family introduced in Sect. 5.3 we provide the initial positions and velocities with 15 digits after the decimal point (see Tables 5, 6).

5.1 Vertical Lyapunov families for equal masses

Beginning with the known equilibrium solutions given by the libration points, the vertical Lyapunov families provide a natural starting point in the study of spatial periodic orbits. Indeed, each libration point in the CRFBP has a pair of purely imaginary eigenvalues associated with the out-of-plane eigenvectors, and we expect these imaginary eigenvalues to give rise to a one-parameter family of periodic out-of-plane oscillations referred to as a vertical Lyapunov family. This family can be computed very accurately near the libration point using a center manifold reduction as discussed in Farrés and Jorba (2010). Beginning from an orbit in the center manifold, we apply a standard numerical continuation scheme and follow the branch. This leads to a large number of numerical orbits, some of which we take as input to our computer-assisted proof.

Table 1 Data for the proofs of the $L_1$ periodic orbits: the table reports an approximate initial condition, an approximate period, and a bound on the $C^0$ distance from the approximate to the true solution. This bound is certified via computer-assisted proof

Table 2 Data for the proofs of the $L_4$ periodic orbits

Table 3 Data for the proofs of the $L_7$ periodic orbits

Table 4 Data for the proofs of the $L_0$ periodic orbits

Table 5 Data (initial positions, periods, and rigorous error bounds) for the proofs of the halo periodic orbits

Table 6 Data (initial velocities) for the proofs of the halo periodic orbits

Table 7 Data for the proofs of the axial periodic orbits

Table 8 Data for the proofs of the axial (pancake) periodic orbits

Figure 5 and Table 1 illustrate the results obtained by applying this strategy at the libration point $L_1$ in the triple Copenhagen problem ($m_1 = m_2 = m_3 = 1/3$). For each orbit, we record an approximate initial condition, the approximate period, and the computer-assisted $C^0$ error bound resulting from our a posteriori analysis. We note that the vertical family at $L_1$ appears to accumulate at the vertical family at $L_0$—the libration point at the origin. The $L_0$ family lies entirely on the z-axis, as the axis is invariant in the triple Copenhagen problem (i.e., there is a four-body version of the Sitnikov problem at the origin). Due to the rotational symmetry of the triple Copenhagen problem, the vertical families at the remaining inner libration points $L_2$ and $L_3$ are obtained by a rotation of $\pm 2 \pi /3$ radians.

Analogous results are given for the vertical Lyapunov families associated with the outer libration points $L_4$ and $L_7$ of the triple Copenhagen problem in Fig. 6 and Table 2 and Fig. 7 and Table 3, respectively. These families appear to pass through the plane of the primaries. We remark that related spatial families of periodic orbits for the CRFBP were studied numerically in Papadakis (2016). We also remark that the vertical Lyapunov families at $L_5$, $L_6$, $L_8$, and $L_9$ are obtained by rotation, giving rise to the data illustrated in Fig. 1.

5.2 A vertical family with non-equal masses

We stress that our method does not make use of any symmetries which may or may not be present in the problem, and because of this, it can be used to prove the existence of non-symmetric orbits. To illustrate this, we consider the CRFBP with mass values $m_1 = 0.4$, $m_2 = 0.35$, and $m_3 = 0.25$, breaking the symmetry of the triple Copenhagen problem. In this case, the z-axis is no longer invariant and we consider the vertical Lyapunov family associated with $L_0$ (which no longer sits at the origin). After computing the center manifold reduction, we perform a numerical continuation of the branch. We prove the existence of 15 periodic orbits obtained in this way. The results are recorded in Fig. 8 and Table 4.

5.3 Spatial orbits bifurcating from planar Lyapunov families: halo and axial families

We recall that the plane of the primaries is an invariant subspace for the CRFBP. Then, another mechanism producing spatial periodic orbits is a symmetry breaking bifurcation for a planar family of periodic orbits Hénon (1973). Natural examples include the planar Lyapunov families associated with the libration points. Indeed, studying bifurcations from the planar Lyapunov families is known to give rise to spatial halo and axial families in the CRTBP. See, for example, Doedel et al. (2007), Calleja et al. (2012), and the references discussed therein.

Taking the CRFBP with non-equal masses $m_1 = 0.4$, $m_2 = 0.3$, and $m_3 = 0.2$—the asymmetric example parameters from Simó (1978)—we start from $L_1$ and perform a center manifold reduction for the in-plane eigenspace associated with the purely imaginary pair of eigenvalues. As in the previous examples, we numerically continue the resulting family until we encounter an out-of-plane stability bifurcation. That is, we track the Floquet multipliers of the periodic orbit and watch for the first bifurcation associated with the out-of-plane bundle (Floquet multipliers pass through a root of unity.) When this occurs an out-of-plane family of periodic orbits may be born (in a pitch-fork bifurcation) and if so we follow the new family via numerical continuation. This leads, for example, to the halo family illustrated in Fig. 9. The results of a number of computer-assisted proofs for this family are given in Tables 5 and 6, where we include precision.

Fig. 5

(Left) $L_1$ family of periodic orbits. (Right) The projection of the same family in the x–y plane. The family appears to accumulate on the z-axis, probably joining with the vertical family associated with $L_0$

Fig. 6

(Left) $L_4$ family of periodic orbits. The periods of the periodic orbits vary from 5.5916 to 7.2211. (Right) The projection of the same family in the x–y plane

Fig. 7

(Left) $L_7$ family of periodic orbits. The periods of the periodic orbits vary from 6.5069 to 7.2274. (Right) The projection of the same family in the x–y plane

Fig. 8

(Left) $L_0$ family of periodic orbits at non-equal masses. The periods of the periodic orbits vary from x to y. (Right) The projection of the same family in the x–y plane

Fig. 9

(Left) Halo family at the mass ratio $m_1=0.5$, $m_2=0.3$, and $m_3=0.2$. The periods of the periodic orbits vary from 4.40766 to 4.04788. (Right) The projection of the same family in the x–y plane

Fig. 10

(Left) Axial family at the mass ratio $m_1=0.5$, $m_2=0.3$, and $m_3=0.2$. The periods of the periodic orbits vary from 7.9168 to 8.2118. (Right) One axial periodic solution with frequency $\omega \approx 0.121776$, that is, with period about 8.2118

Fig. 11

(Left) Pancake family at the mass ratio $m_1=0.5$, $m_2=0.3$, and $m_3=0.2$. The periods of the periodic orbits vary from 4.5763 to 4.6106. (Right) The projection of the same family in the x–y plane

Following the planar Lyapunov family associated with $L_1$ past the first bifurcation, we find other out-of-plane bifurcations, giving rise to additional spatial families which can be followed using numerical continuation. Two more such families are illustrated in Figs. 10 and 11. Applying our method of proof along these branches leads to the certified data reported in Tables 7 and 8. We have also performed some numerical continuations involving the mass parameters, but we believe that including more results in the present work puts us past the point of diminishing returns. Systematic and mathematically rigorous study of continuous branches of periodic orbits—and their bifurcations—in the CRFBP varying mass and energy parameters would make an interesting topic of future study. Just such a study for the halo orbits in the restricted three-body problem has been conducted by Walawska and Wilczak (2018), and those methods could be adapted to the CRFBP as well.

Appendix: Proof of Lemma 3

Since $\gamma$ is a solution of the differential equation, we consider the first, third, and fifth components of the vector field and have that $u_2 = \dot{u}_1$, $u_4 = \dot{u}_3$ and $u_6 = \dot{u}_5$. Moreover, considering the seventh component gives

$$\begin{aligned} \dot{u}_7 = \left( -u_1u_2 - u_3 u_4 - u_5 u_6 + x_1 u_2 + y_1 u_4 + \alpha _1 \right) u_7^3, \end{aligned}$$

and since $u_7 > 0$, we divide by $u_7^3$ and rewrite this as

$$\begin{aligned} \frac{1}{u_7^3} \frac{\mathrm{d}}{\mathrm{d}t}u_7&= -(u_1 - x_1)u_2 - (u_3 - y_1)u _4 - u_5 u_6 + \alpha _1 \\&= -(u_1 - x_1)u_1' - (u_3 - y_1)u _3' - u_5 u_5' + \alpha _1 \\&= - \frac{1}{2} \frac{\mathrm{d}}{\mathrm{d}t}(u_1 - x_1)^2 - \frac{1}{2} \frac{\mathrm{d}}{\mathrm{d}t}(u_2 - y_1)^2 - \frac{1}{2} \frac{\mathrm{d}}{\mathrm{d}t}(u_3)^2 + \alpha _1 \\&= -\frac{1}{2} \frac{\mathrm{d}}{\mathrm{d}t} \left( (u_1 - x_1)^2 + (u_2 - y_1)^2 + u_3^2 \right) + \alpha _1, \end{aligned}$$

or

$$\begin{aligned} \frac{\mathrm{d}}{\mathrm{d}t} G_1(t) = \frac{\mathrm{d}}{\mathrm{d}t} F_1(t) + \alpha _1, \end{aligned}$$

(15)

where

$$\begin{aligned} F_1(t) -\frac{1}{2}\left( (u_1(t) - x_1)^2 + (u_3(t) - y_1)^2 + (u_1(t) - x_1)^2 \right) , \end{aligned}$$

and

$$\begin{aligned} G_1(t) -\frac{1}{2u_7(t)^2}, \end{aligned}$$

are both periodic functions. Taking the average of Eq. (15) over the interval [0, T] leads to

$$\begin{aligned} 0 = \frac{1}{T}\int _{0}^T \alpha _1 \, \mathrm{d}t = \alpha _1, \end{aligned}$$

as the derivatives of $F_1$ and $G_1$ (indeed the derivatives of any periodic function) have average zero. Since $T > 0$, we conclude that $\alpha _1 = 0$ as desired. Nearly identical arguments, applied to the eighth and ninth component equations, show that $\alpha _2 = \alpha _3 = 0$.

Now define

$$\begin{aligned} {\hat{u}}(t) \frac{1}{\sqrt{(u_1(t) - x_1)^2 + (u_3(t) - y_1)^2 + u_5(t)^2}}, \end{aligned}$$

and note that

$$\begin{aligned} \frac{\mathrm{d}}{\mathrm{d}t} {\hat{u}}(t)&= -\frac{\frac{\mathrm{d}}{\mathrm{d}t} (u_1(t) - x_1)^2 + (u_3(t) - y_1)^2 + u_5(t)^2}{2 \left( \sqrt{(u_1(t) - x_1)^2 + (u_3(t) - y_1)^2 + u_5(t)^2}\right) ^3 } \\&= -\,{\hat{u}}^3 \left( (u_1 - x_1) u_2 + (u_3 - y_1)u_4 + u_5 u_6 \right) \\&=-\,{\hat{u}}^3 u_1 u_2 - {\hat{u}}^3 u_3 u_4 -{\hat{u}}^3 u_5 u_6 + {\hat{u}}^3 x_1 u_2 + {\hat{u}}^3 y_1 u_4 . \end{aligned}$$

Then, we see that $u_7(t)$ and ${\hat{u}}(t)$ satisfy the same differential equation with the same initial condition. By existence and uniqueness for ODEs, we have that $u_7(t) = {\hat{u}}(t)$, i.e.,

$$\begin{aligned} u_7(t) = \frac{1}{\sqrt{(u_1(t) - x_1)^2 + (u_3(t) - y_1)^2 + u_5(t)^2}}. \end{aligned}$$

(16)

for all $t\in [0,T]$. Similarly,

$$\begin{aligned} u_8(t) = \frac{1}{\sqrt{(u_1(t) - x_2)^2 + (u_3(t) - y_2)^2 + u_5(t)^2}}. \end{aligned}$$

(17)

and

$$\begin{aligned} u_9(t) = \frac{1}{\sqrt{(u_1(t) - x_3)^2 + (u_3(t) - y_3)^2 + u_5(t)^2}}. \end{aligned}$$

(18)

for all $t\in [0,T]$.

The argument that $\beta = 0$ is similar to the above but different enough that we include it for the sake of completeness. Inspired by the energy functional for the circular restricted four-body problem, we define the function

$$\begin{aligned} H(u) = -(u_2^2 + u_4^2 + u_6^2) + u_1^2 + u_3^2 + 2\left( m_1 u_7 + m_2 u_8 + m_3 u_9 \right) \end{aligned}$$

and observe that $H(\gamma (t))$ is a periodic function. We have that

$$\begin{aligned} \nabla H = \left( \begin{array}{c} 2 u_1 \\ -2 u_2 \\ 2 u_3 \\ -2 u_4 \\ 0 \\ -2 u_6 \\ 2 m_1 \\ 2 m_2 \\ 2 m_3 \end{array} \right) . \end{aligned}$$

Since we have already established that $\alpha _1 = \alpha _2 = \alpha _3 = 0$, we have that

$$\begin{aligned} \left<\nabla H, g \right>&= {\langle }{ \begin{pmatrix} 2 u_1 \\ -2 u_2 \\ 2 u_3 \\ -2 u_4 \\ 0 \\ -2 u_6 \\ 2 m_1 \\ 2 m_2 \\ 2 m_3 \end{pmatrix} \begin{pmatrix} u_2 \\ 2u_4 + u_1 - m_1 u_1 u_7^3 - m_2 u_1 u_8^3 - m_3 u_1 u_9^3 + m_1 x_1 u_7^3 + m_2 x_2 u_8^3 + m_3 x_3 u_9^3 + \beta u_2 \\ u_4 \\ -2 u_2 + u_3 - m_1 u_3 u_7^3 - m_2 u_3 u_8^3 - m_3 u_3 u_9^3 + m_1 y_1 u_7^3 + m_2 y_2 u_8^3 + m_3 y_3 u_9^3 \\ u_6 \\ -m_1 u_5 u_7^3 - m_2 u_5 u_8^3 - m_3 u_5 u_9^3 + m_1 z_1 u_7^3 + m_2 z_2 u_8^3 + m_3 z_3 u_9^3 \\ - u_1 u_2 u_7^3 - u_3 u_4 u_7^3- u_5 u_6 u_7^3 + x_1 u_2 u_7^3 +y_1 u_4 u_7^3 + z_1 u_6 u_7^3 \\ - u_1 u_2 u_8^3 - u_3 u_4 u_8^3- u_5 u_6 u_8^3 + x_2 u_2 u_8^3 +y_2 u_4 u_8^3 + z_2 u_6 u_8^3 \\ - u_1 u_2 u_9^3 - u_3 u_4 u_9^3- u_5 u_6 u_9^3 + x_3 u_2 u_9^3 +y_3 u_4 u_9^3 + z_3 u_6 u_9^3 \end{pmatrix}} {\rangle } \\&= 2 u_1 u_2 -2 u_2 (2u_4 + u_1 - m_1 u_1 u_7^3 - m_2 u_1 u_8^3 - m_3 u_1 u_9^3 + m_1 x_1 u_7^3 + m_2 x_2 u_8^3 + m_3 x_3 u_9^3) - 2 \beta u_2^2 \\&\quad + 2 u_3 u_4 - 2 u_4 (-2 u_2 + u_3 - m_1 u_3 u_7^3 - m_2 u_3 u_8^3 - m_3 u_3 u_9^3 + m_1 y_1 u_7^3 + m_2 y_2 u_8^3 + m_3 y_3 u_9^3) \\&\quad -2u_6 (-m_1 u_5 u_7^3 - m_2 u_5 u_8^3 - m_3 u_5 u_9^3 + m_1 z_1 u_7^3 + m_2 z_2 u_8^3 + m_3 z_3 u_9^3) \\&\quad +2m_1(- u_1 u_2 u_7^3 - u_3 u_4 u_7^3- u_5 u_6 u_7^3 + x_1 u_2 u_7^3 +y_1 u_4 u_7^3 + z_1 u_6 u_7^3) \\&\quad + 2 m_2 (- u_1 u_2 u_8^3 - u_3 u_4 u_8^3- u_5 u_6 u_8^3 + x_2 u_2 u_8^3 +y_2 u_4 u_8^3 + z_2 u_6 u_8^3) \\&\quad +2 m_3 (- u_1 u_2 u_9^3 - u_3 u_4 u_9^3- u_5 u_6 u_9^3 + x_3 u_2 u_9^3 +y_3 u_4 u_9^3 + z_3 u_6 u_9^3 ) \\&= 2 u_1 u_2 -4 u_2 u_4 -2 u_2 u_1 + 2 m_1 u_2 u_1 u_7^3 + 2 m_2 u_2 u_1 u_8^3 + 2 m_3 u_2 u_1 u_9^3 \\&\quad -2 m_1 u_2 x_1 u_7^3 -2 m_2 u_2 x_2 u_8^3 -2 m_3 u_2 x_3 u_9^3 - 2 \beta u_2^2 \\&\quad + 2 u_3 u_4 + 4 u_2 u_4 - 2 u_3 u_4 + 2 m_1 u_3 u_4 u_7^3 + 2 m_2 u_3 u_4 u_8^3 + 2 m_3 u_3 u_4 u_9^3 \\&\quad - 2 m_1 y_1 u_4 u_7^3 - 2 m_2 y_2 u_4 u_8^3 - 2 m_3 y_3 u_4 u_9^3 \\&\quad + 2 m_1 u_5 u_6 u_7^3 + 2 m_2 u_5 u_6 u_8^3 + 2 m_3 u_5 u_6 u_9^3 - 2 m_1 z_1 u_6 u_7^3 - 2 m_2 z_2 u_6 u_8^3 - 2 m_3 z_3 u_6 u_9^3 \\&\quad - 2 m_1 u_1 u_2 u_7^3 - 2 m_1 u_3 u_4 u_7^3 - 2 m_1 u_5 u_6 u_7^3 + 2 m_1 x_1 u_2 u_7^3 + 2 m_1 y_1 u_4 u_7^3 + 2 m_1 z_1 u_6 u_7^3 \\&\quad - 2 m_2 u_1 u_2 u_8^3 - 2 m_2 u_3 u_4 u_8^3 - 2 m_2 u_5 u_6 u_8^3 + 2 m_2 x_2 u_2 u_8^3 + 2 m_2 y_2 u_4 u_8^3 + 2 m_2 z_2 u_6 u_8^3 \\&\quad - 2 m_3 u_1 u_2 u_9^3 - 2 m_3 u_3 u_4 u_9^3 - 2 m_3u_5 u_6 u_9^3 + 2 m_3 x_3 u_2 u_9^3 + 2 m_3 y_3 u_4 u_9^3 \\&\quad + 2 m_3 z_3 u_6 u_9^3. = - 2 \beta u_2^2. \end{aligned}$$

Then, we note that $H(\gamma (t))$ is a periodic function and that the above computation gives

$$\begin{aligned} \frac{\mathrm{d}}{\mathrm{d}t} H(t)&= \nabla H(\gamma (t)) \gamma '(t) \\&= \nabla H(\gamma (t)) g(\gamma (t)) \\&= -2 \beta u_2^2(t). \end{aligned}$$

Taking the average and exploiting that the average of the derivative of a periodic function is zero give

$$\begin{aligned} 0 = \frac{1}{T}\int _0^T \frac{\mathrm{d}}{\mathrm{d}t} H(t) \, \mathrm{d}t = -\frac{2 \beta }{T} \int _0^T u_2(t)^2 \, \mathrm{d}t. \end{aligned}$$

Since $T > 0$ and $u_2(t)^2$ do not change sign, it follows that $\beta = 0$.

Finally, we recall Eqs. (16), (17), and (18) as well as the fact that $\beta = 0$ and have that

$$\begin{aligned} \dot{u}_2&= 2u_4 + u_1 - m_1 u_1 u_7^3 - m_2 u_1 u_8^3 - m_3 u_1 u_9^3 + m_1 x_1 u_7^3 + m_2 x_2 u_8^3 + m_3 x_3 u_9^3 \\&= 2u_4 + u_1 - m_1 (u_1 - x_1) u_7^3 - m_2 (u_1 - x_2) u_8^3 - m_3 (u_1 - x_3) u_9^3 \\&= 2u_4 + u_1 - \frac{m_1 (u_1 - x_1)}{\left( (u_1(t) - x_1)^2 + (u_3(t) - y_1)^2 + u_5(t)^2 \right) ^{3/2}} \\&\quad - \frac{m_2 (u_1 - x_2)}{\left( (u_1(t) - x_2)^2 + (u_3(t) - y_2)^2 + u_5(t)^2 \right) ^{3/2}} \\&\quad - \frac{m_3 (u_1 - x_3)}{\left( (u_1(t) - x_3)^2 + (u_3(t) - y_3)^2 + u_5(t)^2 \right) ^{3/2}} \\&= 2u_4 + {\varOmega }_x. \end{aligned}$$

A similar computation shows that

$$\begin{aligned} \dot{u}_4 = -2 u_2 + {\varOmega }_y \end{aligned}$$

and that

$$\begin{aligned} \dot{u}_6 = {\varOmega }_z. \end{aligned}$$

Then, ${\hat{\gamma }}(t) (u_1(t), u_2(t), u_3(t), u_4(t), u_5(t), u_6(t))$ is a periodic solution of the circular restricted four-body problem as desired.