Provably Stable Neural Dynamics via Koopman Operator Certificates

Learning neural forward models of dynamical systems that remain stable over long rollout horizons is a fundamental challenge in scientific computing and physics-informed machine learning. We introduce Koopman-Stable Neural Dynamics, a deep Koopman architecture whose latent linear dynamics are guaranteed to be Schur stable by construction. The latent transition operator is parameterized as the matrix exponential of a continuous-time generator $G=-S+A$ where $S>0$ is symmetric positive definite and A is skew-symmetric. This yields a native stability certificate: $V(z)=||z||^{2}$ is a strict Lyapunov function requiring no post-hoc verification. We prove that this latent certificate transfers to practical Input-to-State Stability in the original state space under bi-Lipschitz conditions on the encoder-decoder pair, and establish a limitation theorem characterizing when strictly stable embeddings cannot exactly represent a given dynamical system. Experiments on four benchmarks-the Duffing oscillator, an unstable saturating node, the Lorenz attractor, and the ID viscous Burgers' PDE-demonstrate that the certified model maintains bounded predictions where unconstrained baselines diverge catastrophically.