← All papers
First page of Quantitative global regularity for Navier–Stokes equations with odd viscosity on the cubic three-torus

Quantitative global regularity for Navier–Stokes equations with odd viscosity on the cubic three-torus

Jinzheng Li, Yuqi Li, Hao-Yu Sun

math.AP Nov 9, 2026 · v1 math-ph physics.flu-dyn
The three main global-regularity theorems for odd-viscosity Navier–Stokes on the torus are formally verified in Lean 4 with Mathlib, with numerical certificates.
We study the three-dimensional incompressible Navier–Stokes equation on the cubic torus with a constant odd-viscosity operator given by the vertical derivative of the curl. Arbitrary real, mean-zero, divergence-free initial data and an independent steady force, both in the second-order Sobolev space, admit a unique global strong solution when the magnitude of one fixed odd-viscosity coefficient is at least a norm-uniform sufficient threshold. In the unforced case the solution is smooth at positive times. The qualitative argument adapts the resonant-averaging framework for rapidly rotating fluids to the different odd-viscous dispersion. Weighted lattice counts and signed corrected-energy estimates yield a sufficient bound for the odd-to-ordinary viscosity ratio that is polynomial in the normalized initial-data radius at each fixed normalized force radius, together with a separate bound in a specified force-dominated regime. No optimality is claimed for the polynomial exponents or prefactors; determining the sharp viscosity threshold for the original equation remains open. Direct kinetic and weighted enstrophy barriers also give regularity for every coefficient on explicit bounded data and force regions, including the closed unforced ball of homogeneous second-order Fourier Sobolev radius ninety-seven fortieths times the viscosity and seven closed forced rectangles. We specify how finite certificates enter the analytic argument and distinguish minimization of a sufficient formula from sharpness for the original equation. All three main theorems are formally verified in Lean 4 with Mathlib.

Global regularity of the 3D incompressible Navier–Stokes equations on the cubic torus with an odd-viscosity term (vertical derivative of the curl). The question is whether a large enough odd-viscosity coefficient yields global strong solutions for arbitrary H^2 data and force, with quantitative thresholds.

The resonant-averaging framework for rapidly rotating fluids is adapted to the odd-viscous dispersion relation. Weighted lattice counts and signed corrected-energy estimates give a polynomial sufficient bound on the odd-to-ordinary viscosity ratio. Kinetic and weighted enstrophy barriers give regularity for every coefficient on explicit bounded data and force regions. All three main theorems are formalized in Lean 4 with Mathlib, using encoded numerical certificates.

Unique global strong solutions exist once the odd-viscosity coefficient exceeds a norm-uniform threshold, and unforced solutions are smooth at positive times. The barrier arguments give regularity for every coefficient on explicit regions, including an unforced ball of radius 97/40 times the viscosity and seven forced rectangles. The Lean kernel accepts the formalization using only the three standard axioms.