modes
plain-language theorem explainer
modes N assembles the finite set of all 2D Fourier modes with integer wave numbers bounded by N in each direction. Researchers building Galerkin truncations for 2D Navier-Stokes on the torus cite this to index the discrete coefficient space. The body directly builds the set as the Cartesian product of two symmetric integer intervals from -N to N.
Claim. Let $M_N = [(k_1, k_2) : k_1, k_2 : ℤ, max(|k_1|, |k_2|) ≤ N]$. Then modes(N) := $M_N$.
background
The Galerkin2D module develops a finite-dimensional Fourier-mode truncated model for 2D incompressible Navier-Stokes on the torus. Milestone M1 aims to obtain a concrete discrete state space and the basic algebraic energy identity for the inviscid case, without yet treating the continuum limit. Design choices keep the model executable while exposing the analytic content for later milestones.
proof idea
The definition is a direct construction that forms the product of two copies of Finset.Icc on the integer interval from -N to N.
why it matters
This supplies the index set for Galerkin states and is invoked by forty downstream declarations, including coeffAt, coeffAt_add, coeffAt_smul and extendByZero in ContinuumLimit2D, plus numerical checks in VisualBeauty and PhotobiomodulationDevice. It realizes the truncation step of M1 in the ClassicalBridge fluids development and supplies the discrete foundation that can later interface with phi-ladder and J-cost structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.