← All Papers · Formal Verification

The Grade Structure of Navier–Stokes: Why Blowup Requires Grade-2 Saturation

Tamás Nagy, Ph.D. Updated 2026-03-22 Short Draft Formal Verification Lean-Verified
Mathematics verified. Core theorems are machine-checked in Lean 4. Prose and presentation may not have been human-reviewed.
Download PDF View in Graph BibTeX

Abstract

We apply the Latent grade hierarchy to the 3D incompressible Navier–Stokes equations. The key structural observation: NS is an exactly grade-2 system — the right-hand side \(F(u) = \nu\Delta u - \mathbb{P}(u\cdot\nabla u)\) is a polynomial of degree exactly 2 in \(u\), with all higher-grade contributions identically zero. This finite-grade property, combined with the Lean-verified Grade Product Theorem, yields three new results:

(I) High-frequency self-interaction is exponentially suppressed. Decomposing the velocity field into low-grade (\(|k| \leq K\)) and high-grade (\(|k| > K\)) Fourier components, the high-high bilinear interaction satisfies \(\|\mathbb{P}(u_{\text{hi}}\cdot\nabla u_{\text{hi}})\|_{L^2} \leq C_0^2/\rho^{2K}\), where \(\rho\) is the Gevrey analyticity radius. The entire energy cascade mechanism resides in the low-high coupling.

(II) A grade-2 saturation criterion for regularity. Define the grade-2 saturation ratio \(\varepsilon_2(t) = \rho(t)^2 \|\mathbb{P}(u\cdot\nabla u)(t)\|_{L^2}\,/\,C_0(t)\), the fraction of the Cauchy bound consumed by the nonlinearity. We prove: if \(\varepsilon_2(t) < 1\) for all \(t \in [0, T)\), then \(\rho(t) > 0\) and the solution remains analytic on \([0, T)\). Blowup of any Sobolev norm requires \(\varepsilon_2 \to 1\): the nonlinear term must saturate its grade bound. This is a pointwise-in-time criterion that complements the time-integrated Beale–Kato–Majda criterion.

(III) The Reynolds number is a grade ratio. The Reynolds number \(\mathrm{Re} = UL/\nu\) equals the ratio of grade-2 intensity to grade-1 damping: \(\mathrm{Re} = \|B(u,u)\|/\|\nu\Delta u\|\). Turbulence onset (\(\mathrm{Re} \gg 1\)) means grade-2 dominates grade-1. The critical threshold \(\mathrm{Re}_c\) at which the grade hierarchy inverts is the transition to turbulence.

All structural theorems are formalized in Lean 4. We propose DNS diagnostics: tracking \(\varepsilon_2(t)\) during vortex reconnection events in Taylor–Green vortex simulations to empirically characterize the approach to saturation.

Length
4,371 words
Claims
6 theorems
Status
Draft — Active Development
Target
Archive for Rational Mechanics and Analysis / Communications in Mathematical Physics

Connects To

Universal Foundations: A Verified Library of Core Mathematic...

Referenced By

The PDE Tensor Algebra: Structural Decomposition and Exact R... The Kessler Threshold as a Grade-2 Bifurcation: Formally Ver... Grade-2 Dominance Across Millennium Problems: A Unified Stru... Navier-Stokes Regularity Program — Overview

Browse all Formal Verification papers →