extendByZeroLinear
extendByZeroLinear packages the zero-extension of a truncated 2D Galerkin velocity state into the full Fourier coefficient space as a linear map over the reals. Researchers formalizing the passage from finite Galerkin truncations to continuum Fourier states would cite it when they need the algebraic linearity properties made explicit for later compactness arguments. The definition is a direct structure that delegates additivity to extendByZero_add and scalar multiplication to extendByZero_smul.
claimFor each natural number $N$, the map sending a velocity coefficient vector in the truncated space GalerkinState $N$ to its zero-extension in the full Fourier coefficient space FourierState2D is linear over the reals.
background
The module ContinuumLimit2D sets up a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum Fourier limit object. GalerkinState $N$ is defined as EuclideanSpace over the product of the truncated modes and Fin 2, giving the discrete velocity coefficients. FourierState2D is the type of all functions from Mode2 to VelCoeff, representing the infinite Fourier state on the torus. The core embedding function extendByZero populates the full state by zero outside the truncation window, and the sibling lemmas extendByZero_add and extendByZero_smul establish that this embedding preserves addition and scalar multiplication.
proof idea
The definition builds a LinearMap structure whose toFun field is the function extendByZero. It supplies map_add' directly from the lemma extendByZero_add and map_smul' by applying extendByZero_smul followed by simpa to align the scalar-multiplication notation.
why it matters in Recognition Science
This definition supplies the linear structure required by the downstream extendByZeroCLM, which converts the map into a continuous linear map. It fills the explicit embedding step inside the M5 milestone for continuum limits of fluids, keeping the dependency graph visible so that later milestones can replace the surrounding hypotheses with proofs. The construction sits inside the Recognition Science classical bridge and relies on the finite-dimensionality of GalerkinState $N$ to guarantee continuity without additional axioms.
scope and limits
- Does not prove continuity of the resulting linear map.
- Does not establish any convergence of Galerkin sequences in the Fourier space.
- Does not impose or verify the divergence-free condition on the extended state.
formal statement (Lean)
102noncomputable def extendByZeroLinear (N : ℕ) : GalerkinState N →ₗ[ℝ] FourierState2D :=
proof body
Definition body.
103 { toFun := extendByZero
104 map_add' := extendByZero_add (N := N)
105 map_smul' := by
106 intro c u
107 -- `simp` expects `c • x`; our lemma is stated in that form.
108 simpa using (extendByZero_smul (N := N) c u) }
109
110/-- `extendByZero` as a *continuous* linear map.
111
112This is available because `GalerkinState N` is finite-dimensional, hence every linear map out of it
113is continuous. -/