extendByZero
plain-language theorem explainer
The definition maps a finite Galerkin velocity state on the first N modes to an infinite Fourier coefficient field on the torus by zero-padding outside the truncation. Analysts working on Galerkin approximations to Navier-Stokes would cite this embedding when passing to continuum limits. It is realized as a direct functional definition that assembles the two velocity components via the coefficient reader at each mode.
Claim. For a velocity coefficient array $u$ truncated to the finite mode set of level $N$, the zero-extended map $kmapsto (c_0(k),c_1(k))$ returns the Galerkin component $c_j(k)$ when $k$ lies inside the truncation window and the zero vector otherwise.
background
GalerkinState N is the Euclidean space of velocity coefficients indexed by the finite product of the mode set up to N and the two velocity components. FourierState2D is the type of all maps from Mode2 to velocity coefficients, representing the full Fourier expansion on the 2-torus. The auxiliary reader coeffAt extracts one component at a given mode, returning zero when the mode lies outside the truncation. The module ContinuumLimit2D defines the objects and the canonical embedding needed to pass from finite Galerkin trajectories to a candidate continuum limit while packaging analytic compactness steps as explicit hypotheses.
proof idea
Direct definition that, for each mode k, constructs the two-component velocity vector by invoking the coefficient reader on the two Fin 2 indices.
why it matters
This embedding supplies the pointwise convergence data required by the ConvergenceHypothesis structure and by the continuum_limit_exists theorem. It is the concrete map referenced in the module's description of the M5 pipeline that keeps the dependency graph explicit for later replacement of hypotheses by proofs. The construction supports transfer of linear identities from the Galerkin side to the limit object without invoking any Recognition Science constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.