GalerkinState3
plain-language theorem explainer
GalerkinState3(N) supplies the finite-dimensional Euclidean space of Fourier coefficients for the N-truncated velocity field on the three-torus, with one real coordinate per mode per velocity component. Spectral-method researchers working on the incompressible Navier-Stokes equations cite it as the state space for energy identities and enstrophy bounds. The declaration is a direct abbreviation that indexes EuclideanSpace ℝ by the Cartesian product of the modes3 finite set with Fin 3.
Claim. Let $M_N$ be the finite set of wave vectors $k=(k_1,k_2,k_3)∈ℤ^3$ with $|k_i|≤N$ for each $i$. The Galerkin state space is the Euclidean space $ℝ^{M_N×{1,2,3}}$ equipped with the standard $L^2$ inner product.
background
The module extends the two-dimensional Galerkin truncation to three dimensions on the three-torus $T^3$. The function modes3(N) builds the finite set of admissible wave numbers by the Cartesian product of three copies of the integer interval $[-N,N]$. Each element of this set is paired with one of the three velocity components to index the coordinates of the state vector. The local theoretical setting is the spectral Galerkin approximation of the Navier-Stokes equations whose key properties are the energy-skew property of the nonlinearity and the non-positive dissipation of the Laplacian term.
proof idea
This is a one-line abbreviation that applies the modes3 definition to construct the index set (modes3 N) × Fin 3 and then forms the corresponding Euclidean space over the reals.
why it matters
GalerkinState3 supplies the underlying vector space for the convection operator, discrete energy functional, Galerkin right-hand side, and the energy-skew hypothesis. It is the type on which the inviscid energy derivative theorem and spectral enstrophy are defined. In the Recognition Science framework it realizes the Galerkin truncation step referenced in RS_NavierStokes_BKM.tex §4, providing the discrete setting that connects to the sub-Kolmogorov energy cascade analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.