FourierState2D
plain-language theorem explainer
FourierState2D is the type of all maps assigning a real 2-vector velocity coefficient to each 2D Fourier mode on the torus. Workers on Galerkin-to-continuum passages cite it as the target space in which pointwise modewise convergence is stated. The declaration is the direct abbreviation Mode2 → VelCoeff.
Claim. Let Mode$_2 = ℤ × ℤ$ be the set of 2D Fourier modes and VelCoeff = ℝ² the space of velocity Fourier coefficients. FourierState$_{2D}$ is the function space Mode$_2$ → VelCoeff.
background
Module ContinuumLimit2D (Milestone M5) constructs a Lean-checkable pipeline from finite Galerkin approximations on the 2-torus to a candidate continuum limit object. It defines the infinite Fourier coefficient state, the canonical zero-extension embedding of truncated states, and packages compactness and identification steps as explicit hypotheses rather than axioms. Upstream, Mode2 is the type ℤ × ℤ of 2D Fourier modes; VelCoeff is EuclideanSpace ℝ (Fin 2), i.e., a real 2-vector (û₁, û₂); GalerkinState N is the finite-dimensional space of coefficients indexed by the truncated mode set (modes N) × Fin 2.
proof idea
The declaration is a one-line type abbreviation that directly composes the upstream Mode2 and VelCoeff definitions.
why it matters
FourierState2D supplies the codomain for the limit trajectory u in ConvergenceHypothesis and the existential witness in continuum_limit_exists. It therefore anchors the entire family of Duhamel-kernel and dominated-convergence hypotheses that follow. The construction keeps the dependency graph explicit so that later milestones can replace the packaged hypotheses with proofs, consistent with the module's stated goal of honest formalization at M5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.