Tomy Verreault

Top-Down Formalization of Global Smoothness for 3D Incompressible Navier-Stokes Equations in Lean 4: A Zero-Axiom Framework via Osgood's Enstrophy Bound and Beale-Kato-Majda Inequality / Formalisation Top-Down de la Régularité Globale des Équations de Navier-Stokes 3D dans Lean 4 : Un Cadre Sans Axiome via l'Estimation d'Osgood et l'Inégalité de Beale-Kato-Majda

Overview This repository and associated paper present a fully type-checked, Zero-Axiom **Top-Down Formalization Framework** in **Lean 4** and **Mathlib 4** addressing the global existence and smoothness problem for the 3D incompressible Navier-Stokes equations on $\mathbb{R}^3$. Designed under a strict software enginee...