modeTrunc
modeTrunc defines the predicate that a 2D Fourier mode k=(k1,k2) lies inside truncation level N precisely when max(|k1|,|k2|)≤N. Workers constructing finite-mode Galerkin models for 2D Navier-Stokes on the torus cite this predicate to index the discrete coefficient space. The definition is a direct one-line comparison of the integer coordinates against N.
claimFor $N∈ℕ$ and $k=(k_1,k_2)∈ℤ×ℤ$, the predicate holds if and only if $max(|k_1|,|k_2|)≤N$.
background
Mode2 is the type ℤ×ℤ of 2D Fourier wave-vectors on the torus. The module Galerkin2D builds a finite-dimensional model for 2D incompressible Navier-Stokes by restricting to a finite set of these modes; the truncation predicate selects which modes are retained at level N. The companion definition modes(N) assembles the corresponding Finset by ranging over the product of intervals [-N,N] in each coordinate, so that modeTrunc(N,k) is exactly the membership test for that set.
proof idea
One-line definition that directly compares the maximum of the absolute values of the two integer components of k against N.
why it matters in Recognition Science
This predicate supplies the concrete indexing set required by the M1 milestone of the Galerkin2D module, which aims only at a discrete state space and the algebraic energy identity for the inviscid case. It is the membership condition underlying the finite index type ((modes N : Finset Mode2) : Type*) used for coefficient vectors. No downstream theorems are recorded yet; the predicate closes the basic truncation step before nonlinear operators or energy estimates are introduced.
scope and limits
- Does not encode any evolution equation or time-stepping scheme.
- Does not enforce incompressibility or divergence-free conditions on the modes.
- Does not address the continuum limit N→∞ or convergence questions.
- Does not incorporate viscosity, forcing, or boundary conditions.
formal statement (Lean)
37def modeTrunc (N : ℕ) (k : Mode2) : Prop :=
proof body
Definition body.
38 max k.1.natAbs k.2.natAbs ≤ N
39
40/-- The finite set of truncated modes. -/