A Rocq Formalization of Simplicial Lagrange Finite Elements
This work formalizes a foundational concept in finite element methods for numerical analysis, which is incremental as it builds on existing mathematical frameworks but provides a rigorous proof-based implementation.
The authors tackled the formal definition of finite elements in numerical analysis by designing a record in the Rocq proof assistant to represent finite elements with values and proofs of validity, and they instantiated it with simplicial Lagrange finite elements for any dimension and polynomial degree, including the unisolvence proof.
Formalization of mathematics is a major topic, that includes in particular numerical analysis, towards proofs of scientific computing programs. The present study is about the finite element method, a popular method to numerically solve partial differential equations. In the long-term goal of proving its correctness, we focus here on the formal definition of what is a finite element. Mathematically, a finite element describes what happens in a cell of a mesh. It notably includes the geometry of the cell, the polynomial approximation space, and a finite set of linear forms that computationally characterizes the polynomials. Formally, we design a finite element as a record in the Rocq proof assistant with both values (such as the vertices of the cell) and proofs of validity (such as the dimension of the approximation space). The decisive validity proof is unisolvence, that makes the previous characterization unique. We then instantiate this record with the most popular and useful, the simplicial Lagrange finite elements for evenly distributed nodes, for any dimension and any polynomial degree, including the difficult unisolvence proof. These proofs require many results (definitions, lemmas, canonical structures) about finite families, affine spaces, multivariate polynomials, in the context of finite or infinite-dimensional spaces.