A formal proof of the Lax equivalence theorem for finite difference schemes

TL;DR

This paper provides a formal proof of the Lax equivalence theorem for finite difference schemes using the Coq Proof Assistant, establishing convergence conditions based on consistency and stability.

Contribution

It is the first formal proof of the Lax equivalence theorem for finite difference schemes using a proof assistant, with detailed formalization of consistency, stability, and convergence.

Findings

Formal proof of the Lax equivalence theorem using Coq

Demonstration of convergence for a specific difference scheme

Formal verification of consistency and stability conditions

Abstract

The behavior of physical systems is typically modeled using differential equations which are too complex to solve analytically. In practical problems, these equations are discretized on a computational domain, and numerical solutions are computed. A numerical scheme is called convergent, if in the limit of infinitesimal discretization, the bounds on the discretization error is also infinitesimally small. The approximate solution converges to the "true solution" in this limit. The Lax equivalence theorem enables a proof of convergence given consistency and stability of the method. In this work, we formally prove the Lax equivalence theorem using the Coq Proof Assistant. We assume a continuous linear differential operator between complete normed spaces, and define an equivalent mapping in the discretized space. Given that the numerical method is consistent (i.e., the discretization error tends to zero as the discretization step tends to zero), and the method is stable (i.e., the error is uniformly bounded), we formally prove that the approximate solution converges to the true solution. We then demonstrate convergence of the difference scheme on an example problem by proving both its consistency and stability, and then applying the Lax equivalence theorem. In order to prove consistency, we use the Taylor-Lagrange theorem by formally showing that the discretization error is bounded above by the nth power of the discretization step, where n is the order of the truncated Taylor polynomial.