modes3
plain-language theorem explainer
modes3 constructs the finite set of integer wave vectors whose components lie in [-N, N] for the 3D spectral Galerkin truncation of Navier-Stokes on the torus. Researchers deriving a priori energy and enstrophy bounds in finite-dimensional 3D flows cite this index set. The definition is realized directly as the Cartesian product of three integer intervals.
Claim. For each natural number $N$, let $M_N$ be the set of all triples $(k_1,k_2,k_3)inmathbb{Z}^3$ satisfying $|k_i|leq N$ for $i=1,2,3$.
background
Mode3 is the type of wave-number triples, each component an integer, used to index Fourier coefficients of the velocity field on $mathbb{T}^3$. The module extends the 2D Galerkin truncation to three dimensions by retaining only modes inside the cube $[-N,N]^3$, yielding a finite-dimensional approximation in which the convective term is energy-skew and the viscous term is dissipative. Upstream, Mode3 supplies the bare index type with no additional algebraic structure.
proof idea
The definition is a direct construction that forms the product of three copies of the integer interval from $-N$ to $N$ via Finset.Icc and Finset.product, then casts the result to a Finset of Mode3.
why it matters
modes3 supplies the index set for GalerkinState3, the Euclidean space of truncated velocity fields, and is invoked inside spectralEnstrophy and the inner-product identity for the Laplacian. It implements the Fourier truncation step of the Galerkin approximation in RS_NavierStokes_BKM.tex §4, enabling exact verification of the energy identity and the enstrophy bound controlled by $nu N^2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.