kSq3
plain-language theorem explainer
kSq3 computes the squared Euclidean norm of an integer wavevector in the 3D spectral Galerkin truncation of Navier-Stokes. Researchers deriving viscous dissipation or enstrophy bounds in Fourier-mode models would cite this quantity when assembling the discrete Laplacian or spectral energy. The definition is a direct algebraic expansion that sums the squares of the three integer components of the mode.
Claim. For a wave vector $k = (k_1, k_2, k_3) = (k.1, k.2.1, k.2.2) ∈ ℤ³, define $|k|^2 := k_1^2 + k_2^2 + k_3^2$.
background
The module extends the 2D Galerkin truncation to three dimensions on the torus T³ with Fourier modes restricted to the cube [-N, N]³. Mode3 is the type ℤ × ℤ × ℤ that labels these discrete wavevectors. The quantity kSq3(k) supplies the squared wavenumber that multiplies each mode in the viscous term and in the spectral enstrophy sum.
proof idea
The definition is a direct one-line expansion: it projects the three integer components of the Mode3 triple to ℝ and sums their squares. No lemmas are invoked; the expression is the Euclidean norm squared on the integer lattice.
why it matters
kSq3 is the immediate building block for laplacianCoeff3 (which multiplies each coefficient by -kSq3) and for spectralEnstrophy (which weights the L² energy by kSq3). These enter the proofs of laplacianCoeff3_inner_self_nonpos and the enstrophy bound controlled by νN², supporting the energy-skew property and dissipation identity stated in the module documentation for RS_NavierStokes_BKM.tex §4.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.