GalerkinState
plain-language theorem explainer
GalerkinState N supplies the finite-dimensional vector space of velocity coefficients on the truncated Fourier modes for a 2D incompressible Navier-Stokes model on the torus. Researchers working on discrete fluid approximations cite it as the concrete state space on which the projected dynamics and energy identities are defined. The declaration is a direct type abbreviation that identifies the space with Euclidean space indexed by the product of the mode set and the two velocity components.
Claim. For truncation level $N$, let $M_N$ be the finite set of truncated modes. The Galerkin state space is the Euclidean space $E = (M_N) × {0,1} → ℝ$ equipped with the standard inner product, whose elements are the pairs of velocity coefficients for each mode and each spatial component.
background
The module sets up a finite-dimensional Fourier-mode truncated model for 2D incompressible Navier-Stokes on the torus as Milestone M1. The goal is a concrete discrete state space together with the basic algebraic energy identity for the inviscid case, before any continuum limit. The upstream definition modes N produces the finite set of truncated modes as the product of intervals from -N to N in each wave-number direction. The second upstream import supplies the continuum-bridge identification of Laplacian action used later for the heat kernel.
proof idea
This is a one-line type abbreviation that directly constructs the Euclidean space over the index set (modes N) × Fin 2.
why it matters
GalerkinState supplies the state space used by forty downstream declarations in ContinuumLimit2D, including coeffAt, extendByZero, duhamelRemainderOfGalerkin and the associated measurability and Duhamel-integral theorems. It realizes the finite-dimensional truncation step that precedes the continuum limit arguments and supports the algebraic energy conservation identity required for the inviscid case. The construction sits inside the ClassicalBridge domain that connects discrete Recognition Science structures to continuum fluid models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.