laplacianCoeff3
plain-language theorem explainer
The declaration supplies the Fourier multiplier realizing the Laplacian on a 3D spectral truncation of the velocity field. Workers deriving discrete energy dissipation or viscous bounds for Galerkin Navier-Stokes would invoke it when assembling the linear term of the truncated ODE. It is realized by direct pointwise multiplication of each coefficient by the negative squared wave number of its mode.
Claim. For a Galerkin state $u$ on the finite set of modes up to truncation level $N$, the image under the Laplacian is the state whose Fourier coefficients satisfy $v_{k,j} = -|k|^2 u_{k,j}$ for each wave vector $k$ and component index $j$.
background
The module extends the 2D Galerkin construction to three dimensions on the torus with wave vectors restricted to $[-N,N]^3$. GalerkinState3(N) is the Euclidean space whose coordinates are the real Fourier coefficients of the three velocity components indexed by the finite mode set. kSq3(k) returns the squared Euclidean length of the integer triple $k$, while Mode3 is simply the type of such triples. The module document states that the construction yields the energy identity, viscous dissipation, and enstrophy control needed for the discrete sub-Kolmogorov framework in RS_NavierStokes_BKM.tex §4.
proof idea
One-line definition that applies the pointwise map sending each coefficient indexed by mode-component pair kc to the product of -kSq3(kc.1) with the original coefficient.
why it matters
laplacianCoeff3 supplies the viscous contribution inside galerkinNSRHS3, the right-hand side of the truncated evolution equation. It is the direct input to the lemmas laplacianCoeff3_inner_self_nonpos, viscous_energy_nonpos3, viscous_energy_deriv3 and viscous_energy_antitone3 that establish non-positive dissipation of discrete energy for positive viscosity. Within the Recognition Science setting it furnishes the spectral mechanism for the viscous term required by the Galerkin approximation step of the Navier-Stokes analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.