Lean 4 (mathlib) formalization of a concrete R^3 Navier-Stokes stack: certified local existence, unrestricted uniqueness, explicit lifespan, restart/continuation and blow-up dichotomy, plus the actual incompressible NS equations for real divergence-free Schwartz data - with an adversarially audited
Lean Updated 2 months ago 1 commits
sigma-ai|Mirror: HeliCorgi/ns-mns2-flowmap-bridge (⭐0)
2 months agoAbout
Lean 4 (mathlib) formalization of a concrete R^3 Navier-Stokes stack: certified local existence, unrestricted uniqueness, explicit lifespan, restart/continuation and blow-up dichotomy, plus the actual incompressible NS equations for real divergence-free Schwartz data - with an adversarially audited
Readme