A Conditional Physical-Closure Theorem for Three-Dimensional Navier-Stokes

We prove a conditional global regularity theorem for the three-dimensional incompressible Navier–Stokes equations with positive viscosity and real divergence-free initial data in Hγ0(ℝ3), γ0 > 5/2. The hypothesis, which we call a physical window closure, asks that on every time interval inside the lifespan of the strong solution, the size of each Littlewood–Paley shell in the Bradshaw–Grujic frequency window be certified by finite-dimensional data: a finite Fourier dictionary approximating the solution, independent test measurements, a Schur-complement residual bound, an amplitude bound, and a reconstruction error, all dominated by a single time profile with an integrable critical power. Linear algebra from the companion papers returns these certificates to bounds on the actual shells, so the closure makes the Bradshaw–Grujic critical dose finite on every such interval, and the Bradshaw–Grujic continuation criterion then rules out a finite maximal time. The hypothesis is therefore at least as strong as the finiteness of that dose: the theorem derives no new a priori bound from the equations, and it proves neither the closure nor global regularity. Its contribution is the exact certificate form and a checked composition. The return from certificates to the solution and the maximal-time contradiction are formalized in Lean 4, with the Bradshaw–Grujic criterion as an explicit input; the analytic bridges that make that criterion applicable to this solution are written proofs. A record-based route toward the closure, a family of no-go results for shortcuts, and a conditional analyticity branch are analyzed separately and are not used by the theorem.