KAM quasi-periodic tori for the dissipative spin-orbit problem

We provide evidence of the existence of KAM quasi-periodic attractors for a dissipative model in Celestial Mechanics. We compute the attractors extremely close to the breakdown threshold. We consider the spin-orbit problem describing the motion of a triaxial satellite around a central planet under the simplifying assumption that the center of mass of the satellite moves on a Keplerian orbit, the spin-axis is perpendicular to the orbit plane and coincides with the shortest physical axis. We also assume that the satellite is nonrigid; as a consequence, the problem is affected by a dissipative tidal torque that can be modeled as a time-dependent friction, which depends linearly upon the velocity. Our goal is to fix a frequency and compute the embedding of a smooth attractor with this frequency. This task requires to adjust a drift parameter. We have shown in Calleja et al. (2020) that it is numerically efficient to study Poincare maps; the resulting spin-orbit map is conformally symplectic, namely it transforms the symplectic form into a multiple of itself. In Calleja et al. (2020), we have developed an extremely efficient (quadratically convergent, low storage requirements and low operation count per step) algorithm to construct quasi-periodic solutions and we have implemented it in extended precision. Furthermore, in Calleja et al. (2020) we have provided an "a-posteriori"KAM theorem that shows that if we have an embedding and a drift parameter that satisfy the invariance equation up to an error which is small enough with respect to some explicit condition numbers, then there is a true solution of the invariance equation. This a-posteriori result is based on a Nash-Moser hard implicit function theorem, since the Newton method incurs losses of derivatives. The goal of this paper is to provide numerical calculations of the condition numbers and verify that, when they are applied to the numerical solutions, they will lead to the existence of the torus for values of the parameters extremely close to the parameters of breakdown. Computing reliably close to the breakdown allows to discover several interesting phenomena, which we will report in Calleja et al. (2020). The numerical calculations of the condition numbers presented here are not com-pletely rigorous, since we do not use interval arithmetic to estimate the round off error and we do not estimate rigorously the truncation error, but we implement the usual standards in numerical analysis (using extended precision, checking that the results are not affected by the level of precision, truncation, etc.). Hence, we do not claim a computer-assisted proof, but the verification is more convincing than a standard numerics. We hope that our work could stimulate a computer-assisted proof. (c) 2021 Elsevier B.V. All rights reserved.