A Mechanically Verified Census of the Standard Route to the Navier–Stokes Millennium Problem

Abstract

This report presents a mechanical verification census of the Clay Millennium Problem concerning global regularity (or finite-time blowup) of the three-dimensionalincompressible Navier–Stokes equations. Within a proof-checker architecture driven by a symbolic computation kernel (SymPy/mpmath, 30–50 digit precision), we organizeevery provable component of the standard technical route into nineteen machine-replayable verification channels, all of which pass mechanical proof; simultaneously,we dissect the open core of the problem—the supercritical regularity gap—to constant precision. The main machine-proved results include: (i) a complete operator-level replay of the two-dimensional global regularity theorem for general initial data (Ladyzhenskaya’s theorem: stretching operator structurally annihilates + transport orthogonality Fourier mode verification + Sobolev bridge=⇒ enstrophy monotonicity =⇒ global H1/L4 bounds); (ii) sharp closure of the a priori estimate chain (energy inequality → Poincaré → Gronwall → Lp →Schauder) on the Taylor–Green anchor (zero constant loss at every level); (iii) the full three-rung Serrin ladder including the critical endpoint (∞, 3)—the critical L3 norm ∥U∥3 = 11.3389 is computed by N = 32 spectral integration with modulus invariance V (n) = V (1) from the substitution theorem; (iv) the CKN degenerate iteration lemma (purely algebraic bootstrap engine via h(x) = e4x − 4ex + 3 =(ex − 1)2(e2x + 2ex + 3) ≥ 0 =⇒ A(r) ≤ 116A(2r) =⇒ (r/r0)4 geometric decay);(v) a complete classification theorem for linear self-similar blowup profiles (sevenbranch exhaustion of the pressure balance system Kij(1 + si + sj) = 0: solution set = diagonal family ∪ strain-rotation composite family, all infinite energy—nofinite-energy linear self-similar blowup exists); (vi) a two-ended quantitative dissection of the supercritical gap (space-side weight spectrum w(p) = 3/p−3/2: energy saturation w(2) = 0 vs critical blowup w(3) = −1/2; time-side Serrin index supplydemand gap Δs = 2). The census concludes with a two-part statement: provable components fully verified, open core quantitatively bounded—the supercritical gaprequires genuinely new mathematics.