Formalization of the Galerkin Construction for the Two-Dimensional Navier--Stokes Equations in Lean

Abstract

We formalize in Lean 4 the Galerkin construction of global Leray--Hopf weak solutions for the unforced two-dimensional Navier--Stokes equations on arbitrary bounded open domains with no-slip boundary conditions. For every initial datum in the solenoidal \(L^2\) velocity space, the solution has a weakly continuous velocity path, satisfies the weak equation locally in time, and obeys the energy inequality at every time. For rectangles, we also formalize finite-horizon solutions with continuous forcing in the dual energy space. The development includes divergence-free graph spaces, compact spectral coordinates, transport cancellation, Ladyzhenskaya estimates, and simultaneous space--time compactness. The abstract Hilbert-space results apply to evolution equations with a compact energy-to-velocity embedding and a skew trilinear nonlinearity.