mem_modes_iff
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.
claimFor $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 in Recognition Science
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.
scope and limits
- Does not establish dynamical properties or energy conservation for the Navier-Stokes equation.
- Does not address the continuum limit as N tends to infinity.
- Does not extend the truncation to three spatial dimensions or non-periodic domains.
- Does not incorporate viscosity, forcing, or boundary conditions.
formal statement (Lean)
44lemma mem_modes_iff {N : ℕ} {k : Mode2} :
45 k ∈ modes N ↔ k.1 ∈ Finset.Icc (-((N : ℤ))) (N : ℤ) ∧ k.2 ∈ Finset.Icc (-((N : ℤ))) (N : ℤ) := by
proof body
Term-mode proof.
46 simp [modes, and_left_comm, and_assoc, and_comm]
47
48/-!
49## Galerkin state space
50-/
51
52-- We use Euclidean (L²) norms/inner products for energy identities, so we model coefficients
53-- in `EuclideanSpace`, not plain Pi types (which carry the sup norm).
54
55/-- Velocity Fourier coefficient at a mode: a Euclidean real 2-vector (û₁, û₂). -/