mem_modes_iff
plain-language theorem explainer
The lemma establishes that a 2D Fourier mode k belongs to the truncated set modes(N) precisely when both integer components lie in the closed interval from -N to N. Researchers constructing finite Galerkin models of 2D incompressible flow on the torus cite it to verify wave-vector membership in the discrete state space. The proof is a direct one-line simplification that unfolds the product definition of modes and normalizes the conjunction.
Claim. For $N : ℕ$ and $k = (k_1, k_2) ∈ ℤ × ℤ$, $k ∈ modes(N)$ if and only if $k_1 ∈ Finset.Icc(-N, N)$ and $k_2 ∈ Finset.Icc(-N, N)$.
background
The module builds a finite-dimensional Fourier truncation of 2D incompressible Navier-Stokes on the torus. Mode2 is the type ℤ × ℤ for wave vectors (k₁, k₂). The set modes(N) is defined as the Cartesian product of two copies of the integer interval Finset.Icc(-N, N), supplying the finite index set for coefficients in the Galerkin state space. Milestone M1 uses this truncation to obtain an explicit discrete state space and the algebraic energy identity for the inviscid case before any continuum limit is taken.
proof idea
The proof is a one-line simp tactic that unfolds the definition of modes and applies commutativity, associativity, and left-commutativity of conjunction to match the target predicate.
why it matters
The lemma supplies the explicit membership test for the truncated mode set that defines the finite state space in the 2D Galerkin model. It supports subsequent constructions such as GalerkinState, discrete energy, and the convection operator inside the same module. Within Recognition Science it contributes to the classical bridge by furnishing a concrete finite basis for velocity expansions on the torus, consistent with the eight-tick octave and spatial dimension D = 3 of the forcing chain while remaining specialized to two dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.