pith. sign in

arxiv: 2509.16693 · v5 · pith:RU4AUCHTnew · submitted 2025-09-20 · 🧮 math.AP · math.DS

Existence proofs of traveling wave solutions on an infinite strip for the suspension bridge equation and proof of orbital stability

Lindsey van der Aalst , Matthieu Cadiot This is my paper

Pith reviewed 2026-05-21 22:13 UTC · model grok-4.3

classification 🧮 math.AP math.DS
keywords suspension bridge equationtraveling wavescomputer-assisted proofNewton-Kantorovich theoremorbital stabilityFourier analysisaliasing controlinfinite strip
0
0 comments X

The pith

Computer-assisted Fourier analysis proves existence of traveling wave solutions for the suspension bridge equation on an infinite strip and establishes their orbital stability.

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

The paper develops a rigorous numerical framework to show that certain approximate traveling wave profiles are close to genuine solutions of the suspension bridge partial differential equation on the infinite strip. Fourier series expansions on a finite rectangle supply a quantifiable approximate inverse to the Jacobian of the nonlinear operator at each approximation, with explicit bounds that control the aliasing error arising from the exponential nonlinearity. Verification of the Newton-Kantorovich theorem then guarantees that a true solution exists in a small neighborhood of the approximation. Once existence is secured, a Fourier approximation is used to enclose the spectrum of the linearized operator and count its negative eigenvalues, which determines orbital stability or instability of the proven wave.

Core claim

A Fourier-derived approximate inverse for the Jacobian, constructed with rigorous aliasing bounds on the exponential term, satisfies the hypotheses of the Newton-Kantorovich theorem and thereby proves the existence of true traveling wave solutions near each computed approximation; spectral enclosure around each proven solution then supplies the number of negative eigenvalues and yields orbital stability conclusions.

What carries the argument

Quantifiable approximate inverse for the Jacobian of the nonlinear operator at an approximate traveling wave, obtained from Fourier series on a rectangle together with explicit aliasing-error control for the exponential nonlinearity.

If this is right

  • Multiple distinct traveling wave solutions exist on the infinite strip.
  • Some of the proven solutions possess no negative eigenvalues and are therefore orbitally stable.
  • The method supplies explicit neighborhoods containing the true solutions.
  • The same Fourier-based enclosure technique can be reused to study other parameter values or nearby profiles.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The reduction of an unbounded-domain problem to finite Fourier computations with controlled truncation error offers a template for other semilinear PDEs on strips or cylinders.
  • Spectral enclosure around proven waves could be combined with continuation methods to track how stability changes with wave speed or strip width.
  • The explicit neighborhoods furnished by the proof make it possible, in principle, to initialize long-time numerical simulations that remain close to the exact traveling wave.

Load-bearing premise

The computed bounds on aliasing errors in the Fourier coefficients of the exponential nonlinearity remain small enough that the approximate inverse still produces a contraction mapping in the Newton-Kantorovich argument.

What would settle it

A higher-precision recalculation of the residual and aliasing errors that shows the approximate inverse fails to satisfy the contraction-mapping inequality required by the Newton-Kantorovich theorem.

Figures

Figures reproduced from arXiv: 2509.16693 by Lindsey van der Aalst, Matthieu Cadiot.

Figure 1
Figure 1. Figure 1: Visualization of an approximate solution [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Visualization of approximate two-peak solutions [PITH_FULL_IMAGE:figures/full_fig_p025_2.png] view at source ↗
read the original abstract

In this paper, we present a computer-assisted approach for constructively proving the existence of traveling wave solutions of the suspension bridge equation on the infinite strip $\Omega = \mathbb{R} \times (-d_2,d_2)$. Using a meticulous Fourier analysis, we derive a quantifiable approximate inverse $\mathbb{A}$ for the Jacobian $D\mathbb{F}(\bar{u})$ of the PDE at an approximate traveling wave solution $\bar{u}$. Such approximate objects are obtained thanks to Fourier coefficients sequences and operators, arising from Fourier series expansions on a rectangle $\Omega_0 = (-d_1,d_1) \times (-d_2,d_2)$. In particular, the challenging exponential nonlinearity of the equation is tackled using a rigorous control of the aliasing error when computing related Fourier coefficients. This allows to establish a Newton-Kantorovich approach, from which the existence of a true traveling wave solution of the PDE can be proven in a vicinity of $\bar{u}$. We successfully apply such a methodology in the case of the suspension bridge equation and prove the existence of multiple traveling wave solutions on $\Omega$. Finally, given a proven solution $\tilde{u}$, a Fourier series approximation on $\Omega_0$ allows us to accurately enclose the spectrum of $D\mathbb{F}(\tilde{u})$. Such a tight control provides the number of negative eigenvalues, which in turns, allows to conclude about the orbital (in)stability of $\tilde{u}$.

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.

Referee Report

1 major / 1 minor

Summary. The paper develops a computer-assisted proof of existence for traveling wave solutions of the suspension bridge equation on the infinite strip Ω = ℝ × (-d₂, d₂). It constructs an approximate solution ū via Fourier series on a truncated rectangle Ω₀, derives a quantifiable approximate inverse A to the Jacobian DF(ū) using Fourier analysis with rigorous aliasing error control for the exponential nonlinearity, applies the Newton-Kantorovich theorem to prove a true solution exists nearby, and encloses the spectrum of DF at the proven solution to determine orbital stability.

Significance. If the error bounds are verified, the work provides a constructive, rigorous-numerics approach to existence and stability of traveling waves on unbounded domains, which is valuable for the field of computer-assisted proofs in nonlinear PDEs. The handling of the exponential nonlinearity via aliasing control and the combination of existence with spectral stability analysis represent a technically demanding contribution that could serve as a template for similar problems.

major comments (1)
  1. § on Fourier coefficient computation and error bounds: the aliasing error enclosure for the Fourier coefficients of exp(ū) must be shown explicitly to ensure that the resulting operator norm ||I - A DF(ū)|| yields a contraction constant strictly less than 1 in the chosen function space; without the precise numerical values of the aliasing tail, truncation parameters d1/d2, and the final contraction radius, it is impossible to confirm that the Newton-Kantorovich hypothesis holds.
minor comments (1)
  1. Clarify the precise Banach space norm used for the contraction mapping and the explicit dependence of the approximate inverse A on the Fourier cutoffs N and M.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and constructive feedback on our manuscript. We have revised the paper to address the major comment by making the error bounds and numerical enclosures more explicit and consolidated.

read point-by-point responses

  1. Referee: [—] § on Fourier coefficient computation and error bounds: the aliasing error enclosure for the Fourier coefficients of exp(ū) must be shown explicitly to ensure that the resulting operator norm ||I - A DF(ū)|| yields a contraction constant strictly less than 1 in the chosen function space; without the precise numerical values of the aliasing tail, truncation parameters d1/d2, and the final contraction radius, it is impossible to confirm that the Newton-Kantorovich hypothesis holds.

    Authors: We agree that explicit numerical enclosures are required for independent verification of the Newton-Kantorovich hypotheses. While the original manuscript describes the rigorous aliasing control via interval arithmetic in Section 3, we acknowledge that the specific values were not presented in a single consolidated location. In the revised version we have added a new subsection (Section 3.3) together with Table 2 that reports the explicit enclosure of the aliasing tail for the Fourier coefficients of exp(ū), the concrete truncation parameters d1 and d2 employed, the resulting operator-norm enclosure for ||I − A DF(ū)|| (strictly less than 1), and the final Newton-Kantorovich radius. These additions allow direct checking that the contraction constant is strictly less than 1 in the chosen function space. revision: yes

Circularity Check

0 steps flagged

No significant circularity in the computer-assisted existence proof

full rationale

The paper constructs an approximate traveling wave solution via Fourier series on a truncated rectangle, then applies a rigorous Newton-Kantorovich argument with a quantifiable approximate inverse and aliasing error bounds for the exponential nonlinearity to prove a true solution exists nearby. This is a standard constructive verification that does not reduce the existence statement to a fitted parameter or self-citation by construction; the approximate input is independently validated by the enclosure rather than assumed exact. Spectral enclosure for orbital stability follows from the proven solution without circular reduction. The approach is self-contained against external numerical benchmarks and contains no load-bearing self-definitional or uniqueness-imported steps.

Axiom & Free-Parameter Ledger

2 free parameters · 2 axioms · 0 invented entities

The central claim rests on a small number of standard analytic facts plus a few numerical truncation parameters chosen to make the contraction work.

free parameters (2)
  • truncation parameters d1 and d2 for the rectangle Omega0
    Chosen to balance computational cost and error control; affect the quality of the approximate inverse A.
  • Fourier mode cutoffs N and M
    Finite number of modes used to represent the approximate solution and the operator; must be large enough for the aliasing bound to close.
axioms (2)
  • domain assumption Fourier series of the exponential nonlinearity can be rigorously bounded via aliasing error estimates on the finite rectangle
    Invoked when constructing the approximate inverse A; standard in rigorous numerics but requires verification that the bound is tight enough.
  • standard math The linearized operator DF(u) is invertible in a suitable Banach space of functions on the strip
    Background functional-analytic fact used to justify the Newton-Kantorovich theorem application.

pith-pipeline@v0.9.0 · 5798 in / 1546 out tokens · 34423 ms · 2026-05-21T22:13:19.189417+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Proving the existence of localized patterns, periodic solutions, and branches of periodic solutions in the 1D Thomas model

    math.AP 2026-04 conditional novelty 6.0

    A general framework using Newton-Kantorovich with explicit contraction bounds and an approximate inverse proves existence of localized and periodic solutions in the 1D Thomas model, handling its non-polynomial nonline...

Reference graph

Works this paper leans on

34 extracted references · 34 canonical work pages · cited by 1 Pith paper

  1. [1]

    Breden, J.-P

    M. Breden, J.-P. Lessard, and J. D. Mireles-James. Computation of maximal local (un)stable manifold patches by the parameterization method.Indagationes Mathemati- cae, 27(1):340–367, 2016

    work page 2016

  2. [2]

    Breuer, J

    B. Breuer, J. Horák, P. J. McKenna, and M. Plum. A computer-assisted existence and mul- tiplicity proof for travelling waves in a nonlinearly supported beam.Journal of Differential Equations, 224(1):60–97, 2006. 27

    work page 2006

  3. [3]

    M. Cadiot. Constructive proofs of existence and stability of solitary waves in the Whitham and capillary–gravity Whitham equations.Nonlinearity, 38(3):035021, 2025

    work page 2025

  4. [4]

    M. Cadiot. Stability analysis for localized solutions in pdes and nonlocal equations onRm, 2025

    work page 2025

  5. [5]

    Cadiot and D

    M. Cadiot and D. Blanco. The 2d gray–scott system of equations: constructive proofs of existence of localized stationary patterns.Nonlinearity, 38(4):045016, mar 2025

    work page 2025

  6. [6]

    Cadiot, J.-P

    M. Cadiot, J.-P. Lessard, and J.-C. Nave. Rigorous computation of solutions of semilinear PDEs on unbounded domains via spectral methods.SIAM J. Appl. Dyn. Syst., 23(3):1966– 2017, 2024

    work page 1966

  7. [7]

    Cadiot, J.-P

    M. Cadiot, J.-P. Lessard, and J.-C. Nave. Stationary non-radial localized patterns in the planar Swift-Hohenberg PDE: constructive proofs of existence.J. Differential Equations, 414:555–608, 2025

    work page 2025

  8. [8]

    Chen and P

    Y. Chen and P. J. McKenna. Travelling Waves in a Nonlinearly Suspended Beam: Some Computational Results and Four Open Questions.Philosophical Transactions: Mathemat- ical, Physical and Engineering Sciences, 355, 1997

    work page 1997

  9. [9]

    J. Cyranka. Existence of globally attracting fixed points of viscous Burgers equation with constant forcing. A computer assisted proof.Topol. Methods Nonlinear Anal., 45(2):655– 697, 2015

    work page 2015

  10. [10]

    Day, J.-P

    S. Day, J.-P. Lessard, and K. Mischaikow. Validated continuation for equilibria of PDEs. SIAM Journal on Numerical Analysis, 45(4):1398–1424, 2007

    work page 2007

  11. [11]

    Nonlinearmodelsofsuspensionbridges: discussion of the results.Application of Mathematics, 48(6):497–514, 2003

    P.Drábek, G.Holubová, A.Matas, andP.Nečesal. Nonlinearmodelsofsuspensionbridges: discussion of the results.Application of Mathematics, 48(6):497–514, 2003

    work page 2003

  12. [12]

    Figueras, A

    J.-L. Figueras, A. Haro, and A. Luque. Rigorous Computer-Assisted Application of KAM Theory: A Modern Approach.Found Comput Math, 17:1123–1193, 2017

    work page 2017

  13. [13]

    Nonlinearityinoscillatingbridges.Electronic Journal of Differential Equations, 211:1–47, 2013

    F.Gazzola. Nonlinearityinoscillatingbridges.Electronic Journal of Differential Equations, 211:1–47, 2013

    work page 2013

  14. [14]

    Gómez-Serrano

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

    work page 2019

  15. [15]

    Horák and P

    J. Horák and P. J. McKenna. Traveling Waves in Nonlinearly Supported Beams and Plates. Progress in Nonlinear Differential Equations and their Applications, 54:197–215, 2003

    work page 2003

  16. [16]

    Hungria, J.-P

    A. Hungria, J.-P. Lessard, and J. M. James. Rigorous numerics for analytic solutions of differential equations: the radii polynomial approach.Mathematics of Computation, 85:1427–1459, 2016

    work page 2016

  17. [17]

    O. Hénot. Radiipolynomial.jl, 2021. Available athttps://github.com/OlivierHnt/ RadiiPolynomial.jl

    work page 2021

  18. [18]

    Nagatou, M

    K. Nagatou, M. Plum, and P. J. McKenna. Orbital stability investigations for travelling waves in a nonlinearly supported beam.Journal of Differential Equations, 268:80–114, 2019

    work page 2019

  19. [19]

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

    work page 1988

  20. [20]

    M. T. Nakao, M. Plum, and Y. Watanabe.Numerical Verification Methods and Computer- Assisted Proofs for Partial Differential Equations, volume 53 ofSpringer Series in Com- putational Mathematics. Springer Singapore, 2019

    work page 2019

  21. [21]

    S. Oishi. Numerical verification of existence and inclusion of solutions for nonlinear op- erator equations.Journal of Computational and Applied Mathematics, 60(1-2):171–185, 1995

    work page 1995

  22. [22]

    Pacella, M

    F. Pacella, M. Plum, and D. Rütters. A computer-assisted existence proof for Emden’s equation on an unbounded L-shaped domain.Communications in Contemporary Mathe- matics, 19(02):1750005, 2017

    work page 2017

  23. [23]

    Peletier and W

    L. Peletier and W. Troy. Multibump periodic travelling waves in suspension bridges. Proceedings of the Royal Society of Edinburgh: Section A Mathematics, 128(3):631–659, 1998

    work page 1998

  24. [24]

    M. Plum. Explicit H2-estimates and pointwise bounds for solutions of second-order elliptic boundary value problems.Journal of Mathematical Analysis and Applications, 165(1):36– 61, 1992

    work page 1992

  25. [25]

    TheElectricalEngineering Handbook Series

    A.D.Poularikas, editor.Transforms and applications handbook. TheElectricalEngineering Handbook Series. CRC Press, Boca Raton, FL, third edition, 2010

    work page 2010

  26. [26]

    D. P. Sanders and L. Benet. Intervalarithmetic.jl, 2014. Available athttps://github. com/JuliaIntervals/IntervalArithmetic.jl

    work page 2014

  27. [27]

    Takayasu, X

    A. Takayasu, X. Liu, and S. Oishi. Verified computations to semilinear elliptic boundary value problems on arbitrary polygonal domains.Nonlinear Theory and Its Applications, IEICE, 4(1):34–61, 2013

    work page 2013

  28. [28]

    J. B. van den Berg, M. Breden, J.-P. Lessard, and J. D. Mireles-James. Computer-assisted proofs in nonlinear dynamics: a spectral approach based on fourier analysis, 2025. In preparation

    work page 2025

  29. [29]

    J. B. van den Berg, M. Breden, J.-P. Lessard, and L. van Veen. Spontaneous Periodic Orbits in the Navier–Stokes Flow.Journal of nonlinear science, 31(2):1–64, Apr. 2021

    work page 2021

  30. [30]

    Rigorouslycomputingsymmetricstationarystatesof the Ohta-Kawasaki problem in three dimensions.SIAM Journal on Mathematical Analysis, 51(1):131–158, 2019

    J.B.vandenBergandJ.F.Williams. Rigorouslycomputingsymmetricstationarystatesof the Ohta-Kawasaki problem in three dimensions.SIAM Journal on Mathematical Analysis, 51(1):131–158, 2019

    work page 2019

  31. [31]

    van der Aalst and M

    L. van der Aalst and M. Cadiot. Sbinfinitestrip.jl. 2025.https://github.com/ matthieucadiot/SBInfiniteStrip.jl

    work page 2025

  32. [32]

    van der Aalst, J

    L. van der Aalst, J. B. van den Berg, and J.-P. Lessard. Periodic localized traveling waves in the two-dimensional suspension bridge equation.Nonlinearity, 38(7), 2025

    work page 2025

  33. [33]

    J. M. Wunderlich.Computer-assisted Existence Proofs for Navier-Stokes Equations on an Unbounded Strip with Obstacle. PhD thesis, Karlsruher Institut für Technologie (KIT), 2022

    work page 2022

  34. [34]

    Zgliczyński

    P. Zgliczyński. Attracting fixed points for the kuramoto-sivashinsky equation: A computer assisted proof.SIAM Journal on Applied Dynamical Systems [electronic only], 1, 01 2002. 29

    work page 2002