The Evolution of Computer-Assisted Proof In Analysis

TL;DR

This paper investigates how numerical discretization schemes can induce false dynamics in stiff systems and introduces a computer-assisted proof framework to verify the stability of these models, emphasizing the importance of formal safety certifications.

Contribution

It presents a novel framework embedding computer-assisted proofs within the analysis of discretized dynamical systems, using rigorous interval arithmetic and projection techniques.

Findings

Discrete schemes can cause topological bifurcations in stiff systems.

The paper verifies a spurious period-4 sink using rigorous proof methods.

Highlights the need for formal safety verification in learned dynamical models.

Abstract

The intersection of numerical analysis and machine learning, particularly in the domain of Neural ODEs and Physics-Informed Neural Networks (PINNs), relies heavily on discrete approximations of continuous flows. However, in stiff systems, explicit discretization schemes can induce topological bifurcations, creating spurious attractors that do not exist in the underlying continuous dynamics. In this paper, we analyze a stiff 2D nonlinear system integrated via Heun's method, demonstrating how the discrete map undergoes a numerical bifurcation that renders the true equilibrium repelling along an invariant manifold. Adopting a literate programming paradigm where "the paper is the proof," we embed a Computer-Assisted Proof (CAP) directly within the manuscript. Utilizing rigorous complex interval arithmetic and a dimensionality-reducing "Snap-to-Axis" projection, we mathematically verify that a neighborhood of trajectories is permanently captured by a spurious period-4 sink. This work highlights the critical need for formal safety certifications in learned dynamical models and provides a framework for verifying their stability.