kSq
plain-language theorem explainer
kSq computes the squared Euclidean norm of a 2D integer Fourier mode k = (k1, k2). Researchers deriving heat-kernel bounds or Duhamel formulas for spectral Navier-Stokes would cite this when passing from discrete modes to continuum estimates. The definition is a direct coercion of the integer components to reals followed by summing their squares.
Claim. For a Fourier mode $k = (k_1, k_2) = (k.1, k.2) ∈ ℤ × ℤ$, define $kSq(k) := k_1^2 + k_2^2$.
background
The Galerkin2D module constructs a finite-dimensional Fourier-mode truncation of 2D incompressible Navier-Stokes on the torus. Mode2 is the type ℤ × ℤ of 2D Fourier modes (k₁, k₂), with truncation enforced separately by a predicate max(|k₁|, |k₂|) ≤ N. The module isolates algebraic energy identities for the inviscid case before continuum-limit work begins.
proof idea
One-line definition: coerce the integer components of the mode to reals and sum their squares.
why it matters
kSq supplies the scalar |k|² multiplier that appears in every heat-kernel factor exp(-ν |k|² t) and in the Duhamel integral kernels. It is invoked directly in abs_heatFactor_le_one, duhamelRemainderOfGalerkin_kernel, galerkin_duhamelKernel_identity, and extendByZero_laplacianCoeff, thereby linking the discrete Galerkin energy identity to the mild-solution representation of the Stokes equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.