galerkinNSRHS3
plain-language theorem explainer
The definition supplies the right-hand side vector field for the finite-dimensional ODE obtained by projecting the 3D Navier-Stokes equations onto the span of Fourier modes with wave numbers bounded by N. Analysts deriving energy decay and enstrophy bounds for spectral Galerkin approximations cite this construction when passing from the continuous PDE to its truncated system. The definition is a direct algebraic combination of the viscosity-scaled spectral Laplacian and the quadratic convection term.
Claim. For truncation level $N$, viscosity parameter $ν$, convection operator $B$, and state $u$ in the space of Fourier coefficients indexed by modes up to $N$ in each of three directions, the right-hand side is $ν Δu - B(u,u)$, where $Δ$ is the spectral Laplacian that multiplies the coefficient of mode $k$ by $-|k|^2$.
background
The module implements a 3D spectral Galerkin truncation for the Navier-Stokes equations on the 3-torus, extending the 2D version. GalerkinState3(N) is the Euclidean space of Fourier coefficients indexed by modes3(N) × Fin 3, representing the velocity field truncated to wave numbers |k| ≤ N. ConvectionOp3(N) is the type of bilinear maps encoding the projected nonlinearity. laplacianCoeff3 applies the multiplier -kSq3(k) to each Fourier mode of the input state. Energy is simply the real line, serving as the codomain for the discrete energy functional. The module targets the energy identity in which the Galerkin nonlinearity is energy-skew (⟪B(u,u), u⟫ = 0) and viscous dissipation satisfies ⟪u, Δu⟫ ≤ 0.
proof idea
This is a one-line definition that computes the viscous contribution as ν times the spectral Laplacian applied to u, then subtracts the convection operator B applied to the pair (u, u).
why it matters
This right-hand side is the core of the Galerkin ODE whose solutions are analyzed in the downstream theorems viscous_energy_deriv3, viscous_energy_nonpos3, viscous_energy_bound3, and viscous_energy_antitone3. It fills the role of the truncated Navier-Stokes vector field in RS_NavierStokes_BKM.tex §4, enabling proofs that the discrete energy is nonincreasing under positive viscosity. The construction connects to the Recognition Science framework through the discrete energy functional and the control of enstrophy by νN², supporting the sub-Kolmogorov scale analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.