extendByZero_smul
The lemma shows that zero-extension of a truncated Galerkin velocity field commutes with scalar multiplication by any real number. Researchers constructing continuum limits from finite-mode fluid models cite it when verifying that the embedding map is linear. The proof is a direct term-mode computation that reduces the claim to componentwise coefficient identities via extensionality and case analysis.
claimFor any natural number $N$, real scalar $c$, and Galerkin velocity field $u$ with $N$ modes, the zero-extension satisfies $E(c u) = c E(u)$, where $E$ denotes the canonical extension of truncated coefficients to the full Fourier state by setting all higher-mode coefficients to zero.
background
The ContinuumLimit2D module builds a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to an infinite Fourier coefficient state. GalerkinState N is the Euclidean space of real coefficients indexed by the product of the first N modes with the two velocity components. The extendByZero map sends such a truncated state to a full FourierState2D by placing the two components of each retained coefficient into the corresponding mode and setting all other modes to the zero vector.
proof idea
The term proof first invokes classical and funext to obtain pointwise equality on modes, then applies ext to the two-component vector at each mode. The resulting finite cases are dispatched by fin_cases, after which simp reduces each side using the definition of extendByZero together with the companion lemma that coefficients commute with scalar multiplication.
why it matters in Recognition Science
This algebraic compatibility is invoked by extendByZeroLinear to equip the extension with a linear-map structure, and by galerkinNS_hasDerivAt_extendByZero_mode when differentiating the extended Navier-Stokes trajectory. It supplies the vector-space step required at milestone M5 for passing from discrete Galerkin dynamics to continuum Fourier objects while keeping all dependencies explicit.
scope and limits
- Does not establish continuity or boundedness of the extension in any function-space norm.
- Does not verify preservation of the divergence-free constraint under extension.
- Does not address commutation with the nonlinear convection operator.
- Does not treat convergence of Galerkin sequences to a continuum solution.
formal statement (Lean)
88lemma extendByZero_smul {N : ℕ} (c : ℝ) (u : GalerkinState N) :
89 extendByZero (c • u) = c • (extendByZero u) := by
proof body
Term-mode proof.
90 classical
91 funext k
92 ext j
93 fin_cases j <;> simp [extendByZero, coeffAt_smul]
94