kSq3_nonneg
plain-language theorem explainer
The lemma establishes non-negativity of the squared wave number for each Fourier mode in the 3D Galerkin truncation of Navier-Stokes. Researchers deriving dissipation bounds or enstrophy estimates in spectral fluid methods cite this result. The proof is a one-line wrapper that unfolds the definition of kSq3 and applies the positivity tactic to the resulting sum of squares.
Claim. For every integer vector $k = (k_1, k_2, k_3) ∈ ℤ³$, the squared Euclidean norm $|k|² = k₁² + k₂² + k₃² satisfies $|k|² ≥ 0$.
background
In the 3D spectral Galerkin truncation on T³, Mode3 is the type ℤ × ℤ × ℤ of Fourier modes with components in [-N, N]. The function kSq3 maps each such mode to its squared Euclidean norm, defined as the sum of squares of the three integer components. This construction extends the 2D Galerkin setting to three dimensions while preserving the energy identity and viscous dissipation properties required for the discrete sub-Kolmogorov framework.
proof idea
The proof is a one-line wrapper. It unfolds the definition of kSq3, exposing the sum of three squares of real numbers, then invokes the positivity tactic which recognizes that each square is non-negative and their sum is therefore non-negative.
why it matters
The result is invoked directly in laplacianCoeff3_inner_self_nonpos to establish ⟨u, Δu⟩ ≤ 0 and in spectralEnstrophy_nonneg to guarantee non-negativity of the spectral enstrophy sum. It thereby supports the viscous energy dissipation and enstrophy bound listed in the module documentation for RS_NavierStokes_BKM.tex §4. Within the Recognition framework it supplies the non-negativity needed for the discrete energy and enstrophy controls that connect the Galerkin truncation to the sub-Kolmogorov regime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.