galerkinNSRHS
plain-language theorem explainer
The definition supplies the right-hand side for the finite-mode Galerkin approximation to 2D Navier-Stokes, combining viscous diffusion with the abstract nonlinear convection term. Researchers modeling spectral truncations of incompressible flow cite this when deriving discrete energy balances or passing to the continuum limit. The implementation is a direct one-line combination of the precomputed Laplacian coefficients and the bilinear operator B.
Claim. For truncation level $N$, viscosity parameter $ν$, abstract convection operator $B$, and coefficient vector $u$, the right-hand side is $ν Δu - B(u,u)$, where $Δ$ is the Fourier Laplacian acting modewise by multiplication with $-|k|^2$.
background
The module introduces a finite-dimensional Fourier-mode truncated model for 2D incompressible Navier-Stokes on the torus. GalerkinState is the Euclidean space of velocity coefficients indexed by the finite set of modes and the two velocity components. ConvectionOp is an abstract bilinear map from pairs of states to states that will later be instantiated by explicit Fourier convolution plus Leray projection. laplacianCoeff realizes the Fourier Laplacian by scaling each mode coefficient by $-|k|^2$ (see its definition in the same file). The local setting is the discrete-dynamics section of Milestone M1, whose goal is an algebraic energy identity for the inviscid case rather than the continuum limit.
proof idea
The definition is a one-line wrapper that scales the output of laplacianCoeff by the viscosity scalar and subtracts the result of applying the bilinear ConvectionOp to the state with itself.
why it matters
This definition supplies the concrete right-hand side used by all Duhamel-integral identities and remainder bounds in the ContinuumLimit2D module (duhamelRemainderOfGalerkin_integratingFactor, galerkin_duhamelKernel_identity, nsDuhamelCoeffBound_galerkinKernel and their siblings). It realizes the discrete Navier-Stokes dynamics for Milestone M1, enabling the skew-symmetry argument that yields inviscid energy conservation. In the Recognition framework it furnishes the finite-dimensional bridge from spectral emergence to classical fluid equations before the continuum limit is taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.