Mode2
plain-language theorem explainer
Mode2 is the type of 2D Fourier modes on the torus, represented as integer pairs (k1, k2). Researchers constructing Galerkin truncations for 2D Navier-Stokes cite it as the index set for coefficient vectors in the finite-dimensional model. The declaration is a direct type abbreviation with no proof obligations or computational content.
Claim. A 2D Fourier mode is an element of the Cartesian product $k = (k_1, k_2) ∈ ℤ × ℤ$.
background
The Galerkin2D module builds a finite-dimensional Fourier-mode truncation of 2D incompressible Navier-Stokes on the torus. Modes serve as the discrete index set for GalerkinState vectors; the truncation predicate max(|k1|, |k2|) ≤ N is imposed later via the sibling modes N : Finset Mode2. The module imports Mathlib structures for inner-product spaces and finsets to keep the state space executable while exposing the algebraic energy identity for the inviscid case.
proof idea
This is a one-line type abbreviation that directly sets Mode2 equal to the product type ℤ × ℤ.
why it matters
Mode2 supplies the index type for every downstream construction in ContinuumLimit2D, including coeffAt, coeffBound, galerkinForcing, and the uniform-bounds and convergence hypotheses. It realizes Milestone M1 by providing the concrete finite index set needed before the continuum limit is taken. The type therefore anchors the classical bridge that later interfaces with recognition-derived fluid models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.