Grade Decomposition and Gevrey Regularity for Navier-Stokes: A Machine-Checked Path to the Millennium Prize
Summary
We introduce a grade decomposition of the Gevrey energy balance for the incompressible Navier-Stokes equations and formalize a complete three-phase regularity proof path in the Lean 4 proof assistant.
Length
10,362 words
Claims
7 theorems
Status
Working Paper
Target
Annals of PDE / Journal of Mathematical Fluid Mechanics