Neural networks find high-amplitude water-wave candidates, and interval arithmetic plus Lean turn the residual bound into a checkable statement
Synopsis
Physics-informed neural networks could previously show only small residuals at sampled points, not how large the error is over the continuous domain. This pipeline has a network search the Babenko equation in conformal coordinates for high-amplitude gravity–capillary waves, and staged neural corrections, Fourier projection and Newton polishing cut the maximum sampled residual by about seven orders of magnitude. The candidate is then frozen as an explicit trigonometric polynomial, interval arithmetic yields a rigorous uniform bound on the continuous residual, and Lean machine-checks the deductions from that numerical bound to the final residual theorem.
Interpretation
Candidate solutions for strongly nonlinear, high-amplitude water waves can now carry a rigorous continuous-residual certificate rather than only small residuals at sampled points. Physics-informed neural networks could previously produce numerical solutions with very small residuals, but a small sampled residual does not constitute a rigorous bound on the continuous residual or on the error relative to an exact solution. For the frozen explicit trigonometric polynomial, interval arithmetic gives a uniform residual bound at near-machine precision, the same order as the near-double-precision residual observed in the neural stage.
The search runs directly on the Babenko equation in conformal coordinates, with the wave profile, wave speed and, in continuation experiments, the surface-tension parameter learned from the equation itself without training data. The same network architecture and residual-based optimization, paired with different physical and normalization constraints, recovers three high-amplitude solution families: pure-gravity Stokes waves, pure-capillary Crapper waves and gravity–capillary Wilton ripples. Continuing from a high-amplitude Wilton ripple while letting surface tension vary with the profile and speed yields new candidate solutions whose Fourier composition, parameter values and free-surface geometry depart substantially from the Wilton branch.
Certification freezes the neural output as a cosine series with fixed coefficients, after which the proof is independent of network weights and training history. Four error sources — floating-point roundoff, Fourier truncation, aliasing in nonlinear terms, and the passage from grid to continuum — are enclosed within a single explicit bound. Julia/Arb performs the substantive interval computation and exports exact rational endpoints; Lean 4 takes these endpoints as explicit numerical hypotheses and checks the deductions to the final residual theorem, with no sorry placeholders.
Perspective
What is certified is a uniform bound on the Babenko residual of a given finite trigonometric polynomial at fixed rational parameters, together with a positive lower bound on the capillary denominator; this is a residual theorem for the supplied finite series, not an existence or uniqueness theorem for an exact nearby water wave.
The authors note that proving a nearby exact solution exists would additionally require a rigorous inverse bound for the constrained linearized Babenko operator and control of the nonlinear remainder, which are not part of this certificate. Within the accessible numerical continuation range the new candidate family remains intrinsically finite amplitude, which the authors suggest may mean it does not bifurcate from a linear mode, though confirming whether it is genuinely disconnected from the small-amplitude spectrum needs further analysis. Lean does not independently recompute the Arb interval calculation, so the numerical bounds remain trusted inputs to the formal layer.