spectralEnstrophy_nonneg
plain-language theorem explainer
Spectral enstrophy is non-negative for every finite-mode 3D Galerkin state. Researchers on spectral methods for incompressible Navier-Stokes cite this to guarantee the enstrophy functional is well-defined and bounded from below before deriving dissipation estimates. The term proof unfolds the sum definition and invokes non-negativity of each summand via the non-negative wave-number square and coefficient square.
Claim. For any natural number $N$ and any Galerkin state $u$ in the 3D truncated Fourier space, the spectral enstrophy satisfies $0 ≤ ∑_{k,c} |k|^2 |u_{k,c}|^2$, where the sum runs over retained wave-vectors $k$ in the cube $[-N,N]^3$ and the three velocity components $c$.
background
The module extends the 2D Galerkin truncation to three dimensions on the torus $T^3$ with Fourier modes restricted to the cube $[-N,N]^3$. GalerkinState3 $N$ is the Euclidean space of real coefficients indexed by these modes and the three velocity components. The spectral enstrophy is the quadratic form $∑ kSq3(k) (u_{kc})^2$ over the finite index set. The auxiliary result kSq3_nonneg shows that the squared wave-number $kSq3(k)$ is non-negative for every mode. The module documentation states the target enstrophy bound $Σ|k|^2|û_k|^2 ≤ νN^2$ and connects the construction to the discrete sub-Kolmogorov framework.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definition of spectralEnstrophy to expose the explicit Finset sum, applies the general lemma that a finite sum of non-negative reals is non-negative, and verifies each summand is non-negative by multiplying the non-negative value from kSq3_nonneg by the non-negative square of the coefficient.
why it matters
Non-negativity is the first step toward the enstrophy control stated in the module documentation (RS_NavierStokes_BKM.tex §4), which bounds the spectral enstrophy by νN² and links the Galerkin approximation to the Recognition Science treatment of Navier-Stokes. It sits immediately before the inviscid energy conservation section and supplies the lower bound needed for the viscous dissipation identity ⟨u,Δu⟩ ≤ 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.