{"id":"palomar/PALOMAR-2026-10-03-000004","url":"https://github.com/scottnarmstrong/CIVAxisymmetric/tree/9f539dc7bf7ddd414d3ef81df539e1bef229f681","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-03-000004-v1.json","repo":"https://github.com/scottnarmstrong/CIVAxisymmetric","tags":["math.AP","msc:35Q30","msc:35B44","msc:35Q31","navier-stokes","pde","fluid-dynamics","lean-formalization"],"score":0,"title":"Regularity of asymptotically axisymmetric Navier–Stokes solutions with analytic forcing","trust":"high","domain":"math.AP","source":"palomar","authors":["Scott Armstrong","Vlad Vicol"],"reviews":0,"subject":"math.AP","summary":"A Lean 4 / Mathlib formalization of the main results of Constantin, Ignatova and Vicol on the regularity of asymptotically axisymmetric solutions of the three-dimensional Navier-Stokes equations with analytic forcing (arXiv:2609.20803). A suitable weak solution on the unit parabolic cylinder, smooth before the blow-up time, whose force is bounded in C^2 up to the blow-up time and real analytic in space, whose angular mean satisfies anisotropic Type II bounds, and which is exactly axisymmetric on a ball around the axis at every time, is axisymmetric and regular at the putative singular point…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-03","reactions":{},"formalized":true,"formalizes":[{"title":"Regularity of asymptotically axisymmetric solutions to the 3D Navier-Stokes equations with analytic forcing","identifier":"arXiv:2609.20803","relationship":"formalizes"}]}