arxiv: 2605.07500 · v1 · submitted 2026-05-08 · 🧮 math.DS

Recognition: 2 theorem links

· Lean Theorem

Computer-Assisted Proofs in Dynamical Systems: A Case Study of a Heteroclinic Orbit in the Shimizu--Morioka System

Akitoshi Takayasu, Olivier H\'enot

Pith reviewed 2026-05-11 02:05 UTC · model grok-4.3

classification 🧮 math.DS

keywords computer-assisted proofheteroclinic orbitradii polynomialsShimizu-Morioka systemparameterization methodboundary value problemdynamical systemsquasi-Newton operator

0 comments

The pith

Computer-assisted validation proves a transverse heteroclinic orbit exists in the Shimizu-Morioka system.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper applies the radii polynomial approach, an a posteriori method based on contraction of a quasi-Newton operator, to rigorously establish a transverse heteroclinic orbit in the Shimizu-Morioka dynamical system. It validates equilibria and eigenpairs, constructs local invariant manifolds through the parameterization method, and confirms the connecting orbit by solving a boundary-value problem, all with explicit error bounds computed in floating-point arithmetic. The work presents a uniform four-step procedure for each subproblem and supplies Julia code using the RadiiPolynomial library. A sympathetic reader cares because the method converts numerical evidence into a mathematical proof of a specific connecting orbit that implies complex dynamics.

Core claim

The radii polynomial approach provides an a posteriori validation method that establishes the existence of a transverse heteroclinic orbit in the Shimizu-Morioka system by verifying equilibria, eigenpairs, local invariant manifolds via parameterization, and the connecting orbit via a boundary-value problem, all through contraction of a quasi-Newton operator.

What carries the argument

The radii polynomial approach, an a posteriori validation method based on the contraction of a quasi-Newton operator applied to zero-finding problems for equilibria, manifolds, and orbits.

Load-bearing premise

The numerical approximations and a-posteriori bounds computed in floating-point arithmetic are sufficiently accurate that the radii-polynomial inequalities hold and the quasi-Newton operator is a contraction on the chosen function space.

What would settle it

A computation showing that the radii polynomials fail to satisfy the contraction inequalities for the chosen function space would falsify the validation of this specific orbit.

Figures

Figures reproduced from arXiv: 2605.07500 by Akitoshi Takayasu, Olivier H\'enot.

**Figure 1.** Figure 1: Transverse heteroclinic orbit connecting two saddle equilibria of the Shimizu–Morioka system, inside the strange attractor (shown in light grey). newcomers; more experienced readers will find opportunities to improve the code (performance, memory management) and to sharpen the analytical bounds. The difficulty of describing solutions to nonlinear differential equations has long motivated the development of… view at source ↗

read the original abstract

The radii polynomial approach is an a posteriori validation method based on the contraction of a quasi-Newton operator. We apply this strategy to give a computer-assisted proof of a transverse heteroclinic orbit in the Shimizu--Morioka system, validating the equilibria and eigenpairs, the local invariant manifolds via the parameterization method, and the connecting orbit via a boundary-value problem. For each subproblem we present a four-step procedure: $(i)$ zero-finding formulation, $(ii)$ approximate zero, $(iii)$ approximate inverse, and $(iv)$ bound estimates. This highlights the unifying structure behind the a posteriori validation method. Alongside the analysis, we include code snippets implemented in Julia using the RadiiPolynomial library.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This paper supplies a clean, code-supported computer-assisted proof of one specific transverse heteroclinic orbit in the Shimizu-Morioka system.

read the letter

The main takeaway is that the authors have carried out a full a-posteriori validation of a transverse heteroclinic connection. They certify the equilibria and eigenpairs, the local manifolds via parameterization, and the orbit itself as a boundary-value problem, all inside the radii-polynomial framework. The four-step template (zero-finding setup, numerical approximation, approximate inverse, and explicit contraction bounds) is applied uniformly to each piece, and they supply the corresponding Julia snippets that use the RadiiPolynomial library. That combination of structure and runnable code is the useful part of the work. It gives readers a concrete, inspectable example of how the pieces chain together in a chaotic system. The result itself is new for this particular orbit, and the presentation makes the method look reusable without claiming a general theorem. The soft spots are limited. The techniques are established, so the novelty sits mainly in the example and the unified write-up rather than in new theory. The proof rests on the interval bounds being correctly computed in floating point, but that is precisely what the radii-polynomial test is meant to verify, and the library is built for that task. No circularity or internal inconsistency appears in the outline. This is aimed at people who already work with rigorous numerics in dynamical systems. A reader who wants to see a complete, code-backed case study will get direct value from it and can adapt the template. It is worth sending to peer review because the claim is concrete, the method is appropriate, and the code lets referees check the bounds themselves rather than take them on trust.

Referee Report

0 major / 3 minor

Summary. The manuscript applies the radii polynomial approach, an a posteriori validation method based on contraction of a quasi-Newton operator, to prove the existence of a transverse heteroclinic orbit in the Shimizu-Morioka system. It separately validates the equilibria and eigenpairs, the local invariant manifolds via the parameterization method, and the connecting orbit as a boundary-value problem. Each subproblem is treated with a uniform four-step procedure (zero-finding formulation, approximate solution, approximate inverse, and a posteriori bound estimates), and the presentation includes Julia code snippets using the RadiiPolynomial library.

Significance. If the floating-point bounds are correctly implemented and the contraction inequalities hold, the work supplies a rigorous, computer-assisted existence proof for a heteroclinic connection whose numerical evidence is otherwise only suggestive. The explicit four-step template across subproblems illustrates the method's unifying structure and facilitates extension to other problems. The inclusion of executable Julia code is a clear strength for reproducibility and verification.

minor comments (3)

The abstract states that the orbit is transverse, yet the four-step outline for the boundary-value problem focuses on existence; a short paragraph clarifying how transversality is certified (e.g., via a non-vanishing Melnikov-type quantity or eigenvalue condition on the linearized operator) would strengthen the claim.
The code snippets are helpful but omit the precise interval-arithmetic tolerances and the final radii-polynomial values that close the proof; adding a table or appendix listing the key numerical constants (e.g., the radii r and the contraction factor) would improve verifiability.
A brief statement of the computational resources (CPU time and memory) required to obtain the validated bounds would help readers assess practicality for similar problems.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the careful reading of our manuscript and for the positive assessment of the computer-assisted proof for the transverse heteroclinic orbit in the Shimizu-Morioka system. The referee's summary correctly identifies the radii polynomial approach, the four-step validation procedure applied uniformly to equilibria, manifolds, and the connecting orbit, and the inclusion of Julia code using the RadiiPolynomial library. We appreciate the recognition of the method's unifying structure and the value for reproducibility. The recommendation is for minor revision, but the report contains no specific major comments requiring detailed rebuttal.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper applies the standard radii-polynomial a-posteriori validation framework to certify a transverse heteroclinic orbit. Each subproblem (equilibria, eigenpairs, parameterized manifolds, connecting orbit) is cast as an explicit zero-finding problem whose approximate numerical solution is validated by constructing an approximate inverse and deriving explicit contraction bounds via interval arithmetic. These bounds are computed from the approximate data and do not presuppose the existence statement; the radii-polynomial inequalities are independent checks performed after the numerical approximation step. The implementation relies on the external RadiiPolynomial Julia library rather than any self-citation chain or ansatz smuggled from prior author work. No step reduces by construction to a fitted parameter or self-referential definition of the target orbit.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The proof rests on the contraction-mapping theorem applied to a quasi-Newton operator whose bounds are computed numerically; no new entities are postulated and no free parameters are fitted to produce the existence statement.

axioms (1)

standard math Contraction mapping theorem guarantees a unique fixed point when the operator norm of the derivative is less than one inside a ball whose radius is controlled by the radii polynomials.
Invoked to conclude existence from the a-posteriori bounds on the quasi-Newton operator for each subproblem.

pith-pipeline@v0.9.0 · 5426 in / 1393 out tokens · 60065 ms · 2026-05-11T02:05:22.232884+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

39 extracted references · 39 canonical work pages

[1]

The Parameterization Method for Invariant Manifolds: From Rigorous Results to Effective Computations , volume 195 of Applied Mathematical Sciences

Àlex Haro, Marta Canadell, Jordi-Lluís Figueras, Alejandro Luque, and Josep Maria Mon- delo. The Parameterization Method for Invariant Manifolds: From Rigorous Results to Effective Computations , volume 195 of Applied Mathematical Sciences . Springer, Cham, 2016

work page 2016
[2]

Luis Benet, Olivier Hénot, Benoît Richard, and David P. Sanders. IntervalArithmetic.jl. https://github.com/JuliaIntervals/IntervalArithmetic.jl, 2025. Software

work page 2025
[3]

Julia: A fresh approach to numerical computing

Jeff Bezanson, Alan Edelman, Stefan Karpinski, and Viral B Shah. Julia: A fresh approach to numerical computing. SIAM Rev. , 59(1):65–98, 2017

work page 2017
[4]

Cabré, E

X. Cabré, E. Fontich, and R. de la Llave. The parameterization method for invariant manifolds. I. Manifolds associated to non-resonant subspaces. Indiana Univ. Math. J. , 52(2):283–328, 2003

work page 2003
[5]

Cabré, E

X. Cabré, E. Fontich, and R. de la Llave. The parameterization method for invariant manifolds. II. Regularity with respect to parameters. Indiana Univ. Math. J. , 52(2):329– 360, 2003

work page 2003
[6]

Cabré, E

X. Cabré, E. Fontich, and R. de la Llave. The parameterization method for invariant manifolds. III. Overview and applications. J. Differential Equations , 218(2):444–515, 2005

work page 2005
[7]

From the Lagrange triangle to the figure eight choreography: Proof of Marchal’s conjecture

Renato Calleja, Carlos García-Azpeitia, Olivier Hénot, Jean-Philippe Lessard, and Jason D Mireles James. From the Lagrange triangle to the figure eight choreography: Proof of Marchal’s conjecture. Transactions of the American Mathematical Society , 2026. 19

work page 2026
[8]

Ordinary Differential Equations with Applications , volume 34 of Texts in Applied Mathematics

Carmen Chicone. Ordinary Differential Equations with Applications , volume 34 of Texts in Applied Mathematics. Springer, Cham, 3rd edition, 2024

work page 2024
[9]

Makie.jl: Flexible high-performance data visualiza- tion for Julia

Simon Danisch and Julius Krumbiegel. Makie.jl: Flexible high-performance data visualiza- tion for Julia. Journal of Open Source Software , 6(65):3349, 2021

work page 2021
[10]

A rigorous inte- grator and global existence for higher-dimensional semilinear parabolic PDEs via semigroup theory

Gabriel William Duchesne, Jean-Philippe Lessard, and Akitoshi Takayasu. A rigorous inte- grator and global existence for higher-dimensional semilinear parabolic PDEs via semigroup theory. Journal of Scientific Computing , 102(2):62, 2025

work page 2025
[11]

Goldstine

Herman H. Goldstine. A History of Numerical Analysis from the 16th Through the 19th Century, volume 2 of Studies in the History of Mathematics and Physical Sciences . Springer- Verlag, New York, 1977

work page 1977
[12]

Computer-assisted proofs in PDE: a survey

Javier Gómez-Serrano. Computer-assisted proofs in PDE: a survey. SeMA Journal , 76(3):459–484, 2019

work page 2019
[13]

RadiiPolynomial.jl

Olivier Hénot. RadiiPolynomial.jl. https://github.com/OlivierHnt/RadiiPolynomial.jl,

work page
[14]

ShimizuMoriokaTutorial

Olivier Hénot and Akitoshi Takayasu. ShimizuMoriokaTutorial. https://github.com/ OlivierHnt/ShimizuMoriokaTutorial.jl, 2026. Software

work page 2026
[15]

Mireles James

Allan Hungria, Jean-Philippe Lessard, and Jason D. Mireles James. Rigorous numerics for analytic solutions of differential equations: the radii polynomial approach. Mathematics of Computation, 85(299):1427–1459, 2016

work page 2016
[16]

A proof of Jones’ conjecture

Jonathan Jaquette. A proof of Jones’ conjecture. Journal of Differential Equations , 266(6):3818–3859, 2019

work page 2019
[17]

Mireles James, and Christian Reinhardt

Jean-Philippe Lessard, Jason D. Mireles James, and Christian Reinhardt. Computer- assisted proof of transverse saddle-to-saddle connecting orbits for first order vector fields. Journal of Dynamics and Differential Equations , 26(2):267–313, 2014

work page 2014
[18]

Edward N. Lorenz. Deterministic nonperiodic flow. Journal of the Atmospheric Sciences , 20(2):130–141, 1963

work page 1963
[19]

Mitsuhiro T. Nakao. A numerical approach to the proof of existence of solutions for elliptic problems. Japan Journal of Industrial and Applied Mathematics , 5(2):313–332, 1988

work page 1988
[20]

Nakao, Michael Plum, and Yoshitaka Watanabe

Mitsuhiro T. Nakao, Michael Plum, and Yoshitaka Watanabe. Numerical verification meth- ods and computer-assisted proofs for partial differential equations , volume 53 of Springer Series in Computational Mathematics . Springer, Singapore, [2019] ©2019

work page 2019
[21]

Nakao and Yoshitaka Watanabe

Mitsuhiro T. Nakao and Yoshitaka Watanabe. Learning Verified Numerical Computations through Examples: Theory and Implementation . Saiensu-sha, Tokyo, 2011. in Japanese

work page 2011
[22]

Nakao and Nobito Yamamoto

Mitsuhiro T. Nakao and Nobito Yamamoto. Verified Numerical Computations — A Com- putational Challenge to Infinity . Tutorial: Frontiers of Applied Mathematics. Nihon Hyoron Sha, Tokyo, 1998. in Japanese

work page 1998
[23]

Numerical verification of existence and inclusion of solutions for nonlinear operator equations

Shin’ichi Oishi. Numerical verification of existence and inclusion of solutions for nonlinear operator equations. Journal of Computational and Applied Mathematics , 60:171–185, 1995

work page 1995
[24]

Principles of Verified Numerical Computations

Shin’ichi Oishi, editor. Principles of Verified Numerical Computations . Corona Publishing, Tokyo, 2018. in Japanese. 20

work page 2018
[25]

Shin’ichi Oishi and Siegfried M. Rump. Fast verification of solutions of matrix equations. Numerische Mathematik , 90(4):755–773, 2002

work page 2002
[26]

DifferentialEquations.jl – a performant and feature- rich ecosystem for solving differential equations in Julia

Christopher Rackauckas and Qing Nie. DifferentialEquations.jl – a performant and feature- rich ecosystem for solving differential equations in Julia. Journal of Open Research Software, 5(1):15, 2017

work page 2017
[27]

Siegfried M. Rump. INTLAB — INTerval LABoratory. In Tibor Csendes, editor, Devel- opments in Reliable Computing , pages 77–104. Kluwer Academic Publishers, Dordrecht, 1999

work page 1999
[28]

Siegfried M. Rump. Verification methods: Rigorous results using floating-point arithmetic. Acta Numerica, 19:287–449, 2010

work page 2010
[29]

Nakao, and Shin’ichi Oishi

Kouta Sekine, Mitsuhiro T. Nakao, and Shin’ichi Oishi. A new formulation using the Schur complement for the numerical existence proof of solutions to elliptic problems: with- out direct estimation for an inverse of the linearized operator. Numerische Mathematik , 146(4):907–926, 2020

work page 2020
[30]

Shimizu and N

T. Shimizu and N. Morioka. On the bifurcation of a symmetric limit cycle to an asymmetric one in a simple model. Physics Letters A , 76(3):201–204, 1980

work page 1980
[31]

Theory of an interval algebra and its application to numerical analysis

Teruo Sunaga. Theory of an interval algebra and its application to numerical analysis. RAAG Memoirs , 2:29–46, 1958. Reprinted in Japan J. Ind. Appl. Math. 26 (2009), 125– 143

work page 1958
[32]

Rig- orous numerics for nonlinear heat equations in the complex plane of time

Akitoshi Takayasu, Jean-Philippe Lessard, Jonathan Jaquette, and Hisashi Okamoto. Rig- orous numerics for nonlinear heat equations in the complex plane of time. Numerische Mathematik, 151(3):693–750, 2022

work page 2022
[33]

Trefethen

Lloyd N. Trefethen. Approximation theory and approximation practice. Society for Industrial and Applied Mathematics (SIAM), Philadelphia, PA, 2013

work page 2013
[34]

A rigorous ODE solver and Smale’s 14th problem

Warwick Tucker. A rigorous ODE solver and Smale’s 14th problem. Foundations of Com- putational Mathematics , 2(1):53–117, 2002

work page 2002
[35]

Galerkin’s procedure for nonlinear periodic systems

Minoru Urabe. Galerkin’s procedure for nonlinear periodic systems. Archive for Rational Mechanics and Analysis , 20:120–152, 1965

work page 1965
[36]

Mireles James, and Christian Reinhardt

Jan Bouwe van den Berg, Jason D. Mireles James, and Christian Reinhardt. Comput- ing (un)stable manifolds with validated error bounds: Non-resonant and resonant spectra. Journal of Nonlinear Science , 26(4):1055–1095, 2016

work page 2016
[37]

A proof of Wright’s conjecture

Jan Bouwe van den Berg and Jonathan Jaquette. A proof of Wright’s conjecture. Journal of Differential Equations , 264(12):7412–7462, 2018

work page 2018
[38]

Rigorous Numerics in Dynam- ics, volume 74 of Proceedings of Symposia in Applied Mathematics

Jan Bouwe van den Berg and Jean-Philippe Lessard, editors. Rigorous Numerics in Dynam- ics, volume 74 of Proceedings of Symposia in Applied Mathematics. American Mathematical Society, Providence, RI, 2018

work page 2018
[39]

A numerical verification method for solutions of boundary value prob- lems with local uniqueness by Banach’s fixed-point theorem

Nobito Yamamoto. A numerical verification method for solutions of boundary value prob- lems with local uniqueness by Banach’s fixed-point theorem. SIAM Journal on Numerical Analysis, 35(5):2004–2013, 1998. 21

work page 2004