Special Session 162: Computer-Assisted Proofs in Dynamical Systems

Rigorous global search of all solution orbits for nonlinear boundary value problems

Taisei Asai Yamagata University Japan Co-Author(s):    Kazuaki Tanaka, Satoshi Tanaka, Shin`ichi Oishi

Abstract: Nonlinear boundary value problems often exhibit rich bifurcation structures and may possess multiple solutions. From a dynamical systems perspective, such problems can be interpreted as orbit problems: solutions correspond to trajectories of an associated differential equation that satisfy prescribed boundary conditions. In this formulation, determining all solutions amounts to identifying all admissible solution orbits of the underlying dynamical system. In this talk, we present a computer-assisted framework for the rigorous global search of all such solution orbits. A central difficulty in this search is that the parameters determining trajectories, such as initial conditions in a shooting formulation, typically range over a noncompact set, making direct exploration infeasible. To overcome this difficulty, we first derive a priori bounds that confine all possible solutions to a compact set of initial conditions. This significantly reduces the set of candidates. On this set, we use the kv library to rigorously prove the existence or nonexistence of solutions. This approach allows us to systematically enumerate all solution orbits within a given parameter range. As an application, we present results for nonlinear elliptic problems including H\`{e}non-type equations and discuss the resulting bifurcation structures.

Validated Numerics Guided by Symbolic Computations: A Hybrid Newton-Puiseux Algorithm

Florent BREHARD CRIStAL, CNRS, Universite de Lille France Co-Author(s):    Fabien Corinaldesi, Adrien Poteaux

Abstract: Computing the Puiseux series of complex plane algebraic curves is a cornerstone of computational algebraic geometry, with applications ranging from robotics to theoretical physics. While the Newton-Puiseux algorithm provides a rigorous framework for desingularization, its practical efficiency is often limited by the prohibitive cost of exact arithmetic over algebraic number fields. Conversely, purely numerical approaches struggle with the inherent instability of singularities, where infinitesimal perturbations can collapse the branching structure of the curve. This work proposes a hybrid symbolic-numeric strategy that leverages validated numerics to compute rigorous interval representations of Puiseux coefficients while bypassing the cost of computing with exact algebraic numbers. Our approach utilizes the modular-numeric strategy introduced in Poteaux`s thesis, where the structure of the Puiseux series is first inferred from an execution of Newton-Puiseux over a finite field, by choosing an appropriate prime number. This structural data is encoded into a polygon tree, which is then used as a blueprint guiding the numerical phase. To bridge the symbolic-numeric gap, we develop routines called filters to correctly associate the recursive calls of the numeric algorithm with the branches of these trees, thus ensuring the preservation of Newton polygons and multiplicities at every step. By doing so, we achieve a certified result where traditional interval methods alone would otherwise fail to capture the structure of the singularity. This work demonstrates how the synergy between computer algebra and validated numerics can resolve highly sensitive singular problems with both speed and mathematical rigor.

A Computer-Assisted Proof of Marchal`s Conjecture in the Three-Body Problem

Renato C Calleja IIMAS-UNAM Mexico Co-Author(s):    Olivier H\`enot, Carlos Garc\`ia-Azpeitia, Jean-Philippe Lessard, Jason Mireles James

Abstract: The figure-eight choreography and the equilateral triangle solution are two remarkable periodic motions in the equal-mass three-body problem. In 2000, C.~Marchal conjectured that they belong to the same continuation class, namely the highly symmetric $P_{12}$ family of relative periodic solutions in a rotating frame. In this talk I will describe a computer-assisted proof of this conjecture. After exploiting the symmetries of the problem, the search for choreographic solutions reduces to a delay differential equation for a single body in rotating coordinates. The formulation is singular at both ends of the family, corresponding to the figure-eight and the Lagrange triangle, so the proof combines symmetry reduction with suitable desingularizations at the two endpoints. The main step is an a posteriori validation argument proving the existence of an analytic branch of periodic solutions on the whole parameter interval. The proof uses validated numerics, Fourier-Chebyshev expansions, and interval arithmetic. This is joint work with Olivier H\`enot, Carlos Garc\`ia-Azpeitia, Jean-Philippe Lessard, and Jason Mireles James.

Instability of the 2D Taylor-Green vortex

Gonzalo Cao-Labora EPFL Switzerland Co-Author(s):    Maria Colombo, Michele Dolce, Paolo Ventura

Abstract: A Hamiltonian operator is a linear operator which can be written as JH with J skew-adjoint and H self-adjoint. We will discuss a new criterion to characterize stability and instability of Hamiltonian linear operators when H has finitely many negative directions. This criterion can be used with pen and paper mathematics to prove real instabilities, or combined with computer-assistance to prove complex instabilities. We will focus on the latter case, proving instability of certain stationary solutions of the 2-d Euler equations. More concretely, we prove the conjectured instability of the Taylor-Green vortex (or cellular flow). Our proof relies on finding zeros of a holomorphic function, using an interval arithmetic version of the Cauchy integral formula. Moreover, the computation of our holomorphic function involves a resolvent, where we capitalize on the fact that the Taylor-Green linear dynamics are local in frequency and employ a primal-dual bound to control the distance between the true resolvent and a numerical guess. We expect part of our framework to be applicable to a wider class of linear stability problems where the operator can be decomposed as the sum of a stable infinite-dimensional part plus a finite rank term causing instability.

Computer-Assisted Proofs in Random Dynamical Systems

Maximilian Engel University of Amsterdam Netherlands Co-Author(s):    Maxime Breden

Abstract: I will summarize results from recent years on how to use computer-assisted proofs in random dynamical systems. This will concern rigorous estimates on Lyapunov exponents as indicators of synchronization or chaos as well as large deviation estimates on finite-time Lyapunov exponents as indicators of random bifurcations. The talk will also address new questions and challenges from random dynamical systems that may be approached with rigorous numerics.

On the computation of Tori and their bifurcations

Jordi Lluis Figueras Dept Mathematics Uppsala University Sweden Co-Author(s):

Abstract: We present a computational framework for locating and continuing reducible, normally hyperbolic invariant tori with quasiperiodic internal dynamics in autonomous ordinary differential equations. The method is based on the parameterization method in a Newton-KAM formulation: the torus embedding, its normal bundle, the associated reducibility data, and selected system parameters are solved for simultaneously. Prescribing the internal frequency vector turns the search for invariant tori into a functional equation with small divisors, which we solve by Fourier-based cohomological equations adapted to dissipative flows. A pseudo-arclength continuation strategy is incorporated to detect and traverse quasiperiodic saddle-node bifurcations of invariant tori, including formulations with a distinguished normal direction. The algorithms are designed for high-dimensional systems, where direct discretizations or Poincare-map approaches become expensive or ill-conditioned. We discuss their implementation in a C++ library and illustrate the approach on benchmark examples that exhibit convergence, continuation through folds, and robust computation of hyperbolic bundles. Although the present work is primarily numerical, the formulation is explicitly tailored to a posteriori validation, making it a natural stepping stone toward computer-assisted proofs for quasiperiodic invariant structures and their bifurcations in dissipative dynamical systems. The same framework also avoids normal-form reductions and works directly with the original vector field equations.

An ellipsoidal satellite`s chaotic tumbling model

Anna Gierzkiewicz Jagiellonian University in Krakow Poland Co-Author(s):    Amadeu Delshams, Piotr Zgliczy\\`{n}ski

Abstract: We study the triaxial inner rotation (tumbling) of an ellipsoidal satellite in a Keplerian orbit. In our previous paper we considered a simplified uniaxial case, with the axis of rotation perpendicular to the orbital plane. The system of three ordinary differential equations is periodic with respect to one of the variables (true anomaly $f$), which allowed us to study the Poincar\`e section $f=0=2\pi$. The system exhibited chaotic behavior for some parameters (the shape of the ellipsoid and the orbital eccentricity $e$). We are particularly interested in the values corresponding to Hyperion, one of Saturn`s moons, known for its non-spherical shape and apparently chaotic inner rotation. The uniaxial model does not provide a full physical description of Hyperion`s tumbling, which is clearly triaxial. The full model, based on Euler`s rigid-body equations, leads to a much more complicated system of seven ordinary differential equations (omitted here for reasons of size), of which the simplified uniaxial model is an invariant subspace. For this reason, it too is chaotic, but we expect the structure of this chaos to be more complex in the 7-dimensional space: perhaps it is divided into chaotic regions connected by homo- and heteroclinic orbits. Using the Interval Newton Method implemented in C++ with the use of CAPD library for computer-assisted proofs, we found a number of periodic orbits for the analogous Poincar\`e map in the full space. The current work is to study the behavior of their weakly stable and unstable manifolds which seem to intersect transversely with the help of system`s symmetries. This, in turn, we expect to prove rigorously with CAPD.

Modified parameterization methods in computer-assisted proofs for KAM theory

Alex Haro Universitat de Barcelona & CRM Spain Co-Author(s):    Jordi-Lluis Figueras

Abstract: Computer-assisted proofs combine analytical arguments, rigorous numerics, and validated error bounds to turn high-precision computations into fully mathematical results. Improved analytic arguments lead directly to stronger and more efficient computer-assisted proofs, by producing less restrictive validation criteria and increasing the applicability of CAPs to concrete dynamical systems. In this talk, we discuss this paradigm in the context of KAM theory from the perspective of parameterization methods, where a posteriori invariance equations provide a natural framework to validate numerically computed invariant tori. We present new results in the form of more refined estimates, leading to more effective validation procedures. This is joint work with Jordi-Llu\`is Figueras (Uppsala University).

Efficient implementation of affine arithmetic for rigorous integration of delay differential equations

Ryoga Iwanami Waseda University Japan Co-Author(s):

Abstract: In this talk, we introduce an efficient implementation of affine arithmetic. To compute tight enclosures of trajectories of dynamical systems, it is essential to suppress the wrapping effect. Although affine arithmetic can effectively reduce the wrapping effect, it tends to require significantly longer computation time compared to other methods. To address this issue, we accelerated affine arithmetic by utilizing error-free transformation, SIMD vectorization, and mixed-precision arithmetic. We will demonstrate its effectiveness by applying the accelerated implementation to several dynamical systems.

Validated matrix multiplication transform for orthogonal polynomials with applications to computer-assisted proofs for PDEs

Jonathan Jaquette New Jersey Institute of Technology USA Co-Author(s):    Matthieu Cadiot, Jonathan Jaquette, Jean-Philippe Lessard, Akitoshi Takayasu

Abstract: In this talk, we develop computational tools related to the rigorous computational analysis of nonlinear PDEs posed on geometries such as disks and cylinders. First, we introduce a validated Matrix Multiplication Transform (MMT) algorithm, analogous to the discrete Fourier transform, which offers a reliable framework for evaluating nonlinearities in spectral methods while effectively mitigating challenges associated with rounding errors. Second, we examine the Zernike polynomials, a spectral basis well-suited for problems on the disk, and highlight their essential properties. We further demonstrate how the MMT approach can be effectively employed to compute the product of truncated Zernike series, ensuring both accuracy and efficiency. Finally, we combine the MMT framework and Zernike series to construct computer-assisted proofs that establish the existence of solutions to two distinct nonlinear elliptic PDEs on the disk.

Structures Behind Blow-Up: Algebraic-Geometric Perspectives for Computer-Assisted Proofs

Kaname Matsue Institute of Mathematics for Industry / International Institute for Carbon-Neutral Energy Research, Kyushu University Japan Co-Author(s):    Kaname Matsue

Abstract: In this talk, we discuss methods for computing blow-up solutions of ordinary differential equations in a simple and efficient manner. Broadly speaking, there are two main approaches: one assumes the leading-order term in the asymptotic expansion of blow-up solutions, while the other reduces the problem to the construction of local stable manifolds of bounded invariant sets via compactification of the phase space. Here we examine algebraic and geometric correspondences of blow-up solutions that enable computer-assisted proofs with reduced validation estimates, while ensuring the existence of solutions with various asymptotic behaviors. In particular, the correspondence between these approaches provides different types of stability information, offering useful insights for more advanced analysis as well as numerical computation. This talk focuses on the underlying mathematical framework relevant to computer-assisted proofs and does not address the latest results in computer-assisted validation.

Symbolic dynamics in Pseudospectral projection of Delay Differential Equations

Robert Szczelina Jagiellonian University Poland Co-Author(s):

Abstract: We study the following class of Delay Differential Equations (DDEs): \begin{align*} x`(t) &= f(x(t), x(t-\tau)) & t \ge 0 \ x(t) &= \psi(t) & t \in [-\tau, 0], \end{align*} with $\tau > 0$ fixed, $x \in \mathbb{R}^d$, $\psi \in \mathcal{C}^0([-\tau, 0], \mathbb{R}^d) =: \mathcal{C}$. While significant work has been done on the dynamics of such systems--most notably regarding chaos in the Mackey-Glass equation--the infinite-dimensional nature of DDEs presents some challenges for carrying out the rigorous computations and obtaining estimates good enough for computer-assisted proofs remains a challenge. This talk will present a recent attempt to reduce the number of unknown factors affecting the quality of rigorous numerics by using a pseudospectral approximation, which reduces the DDE to a relatively small system of ODEs while preserving numerically observed dynamical features. Due to the low-dimensionality of the resulting approximation and its great theoretical accuracy, the computations are less demanding and can be done using known tools, such as CAPD, to efficiently verify some dynamical phenomena that closely mirror those of the full system. We present a proof of existence of symbolic dynamics in the ODE approximating DDE and we discuss lessons learned that might be used to guide a similar proof for the full DDE system. The author acknowledge the support of Polish National Science Center (NCN) grant no. 2023/49/B/ST6/02801.

Multi-stepping scheme for rigorous integration of semilinear parabolic PDEs

Akitoshi Takayasu University of Tsukuba Japan Co-Author(s):    Jean-Philippe Lessard

Abstract: In this talk, we present an improved integrator for the study of solutions to initial and boundary value problems for semilinear parabolic PDEs. Our method is based on a non-autonomous semigroup approach, in which the solution map of the linearized PDE along a numerically computed approximate solution is rigorously controlled. In particular, the use of a multi-stepping scheme, based on a new construction of the multi-step propagator via direct backward iteration, allows us to integrate over much longer time intervals. For each time step, we split the dynamics into a signed finite-dimensional bare propagator and a finite-tail coupling correction. The bare propagators are composed at the signed matrix level, which preserves cancellation effects and significantly reduces the wrapping effect. We also present examples for both initial value problems and boundary value problems, including long-time rigorous integration of the Ohta--Kawasaki equation.

Computer-assisted bifurcation point validation

Thomas Wanner George Mason University USA Co-Author(s):    Maxime Breden, Evelyn Sander

Abstract: Parabolic partial differential equations are fundamental models for many applied phenomena. For example, pattern formation in diblock copolymers is described by the evolution of the fourth-order Ohta-Kawasaki equation, while competition in the interaction of populations can be modeled by second-order reaction-diffusion systems such as the Shigesada-Kawasaki-Teramoto model. Essential for a deeper understanding of the long-term dynamics of such problems are the sets of equilibria as described by the associated bifurcation diagrams. In this talk, we present computer-assisted proof techniques which can be used to validate and continue bifurcation points through the use of suitable extended systems. This includes not only fold points, but also pitchfork and transcritical bifurcations which are the result of group actions beyond forcing through involutions. Our results apply to both one- and two-dimensional domains, and they can also be used to treat certain bifurcation points with higher-dimensional kernels.