A Conditional Spectral-Closure Theorem for Three-Dimensional Navier–Stokes

We prove a conditional global theorem for three-dimensional incompressible Navier–Stokes with positive viscosity and real divergence-free Hγ(ℝ3) data, γ>5/2. The hypothesis, a spectral closure on the actual maximal mild solution, asks that on each finite horizon one Fourier cutoff and one fraction strictly below one bound the squared high-frequency part of the strong norm by that fraction of the whole at every existing time. Kinetic energy bounds the low-frequency part, so orthogonal decomposition bounds the full strong norm and rules out a finite maximal time. The same mild path is then a classical solution: it attains the initial velocity, is spatially smooth for positive time, has the first and second time derivatives stated in the theorem, and satisfies the Navier–Stokes equations pointwise with a pressure. The closure is not derived from arbitrary data; with the energy bound it amounts to an a priori bound on the strong norm, and on solutions that never vanish it is equivalent to global existence, so the theorem is the classical continuation principle in spectral form and does not reduce the regularity problem to an easier estimate. An alternative conditional theorem assumes, for some 0<ε<1, finite Fourier certificates whose sizes are bounded by a majorant integrable in time with exponent 2/(1 − ε) over every possible preterminal horizon, together with a terminal form of the Bradshaw–Grujic criterion that is assumed, not derived. An empty certificate pays every horizon inside a global lifespan, so under that terminal hypothesis the closure is equivalent to global existence; the terminal hypothesis must be justified for the chosen frequency windows, since for empty windows it alone excludes a finite maximal time. The paper also records a route that aims to derive such bounds from the equations, together with no-go results and admission rules for its shortcuts; it establishes neither closure. Both conditional theorems are formalized in Lean 4 with Mathlib (the second without its positive-time smoothing addition); an appendix states, result by result, which of the other statements are formalized and which rest on written proofs or stated hypotheses.