extendByZero_neg
plain-language theorem explainer
The lemma asserts that zero-extension of a negated N-mode Galerkin velocity field equals the negation of its zero-extension. Analysts studying the passage from discrete Galerkin models to continuum Navier-Stokes solutions cite this when verifying that the embedding preserves linear operations. The proof reduces negation to scalar multiplication by -1 and applies the scalar-linearity property of the extension map.
Claim. Let $N$ be a natural number and let $u$ be a velocity field in the $N$-mode Galerkin truncation (coefficients in Euclidean space over the product of modes and two components). Then the zero-extension of $-u$ to the full Fourier coefficient state equals the negative of the zero-extension of $u$.
background
The module ContinuumLimit2D constructs a Lean-verifiable bridge from finite Galerkin approximations in 2D to a continuum Fourier state. A GalerkinState $N$ consists of velocity coefficients on the truncated modes together with two components. The map extendByZero pads these coefficients with zeros to produce a full FourierState2D. This lemma is one of several that establish the embedding as a linear map. It relies on the companion result that extendByZero commutes with scalar multiplication. The local setting is the M5 milestone, which keeps the analytic compactness steps as explicit hypotheses while making the algebraic embedding properties fully proved.
proof idea
The proof is a one-line wrapper in term mode. It applies the classical tactic, rewrites negation as scalar multiplication by $-1$ via neg_one_smul, and invokes the already-proved scalar-multiplication lemma extendByZero_smul at scalar $-1$.
why it matters
This lemma supports the differentiability result galerkinNS_hasDerivAt_extendByZero_mode, which shows that the time derivative of the extended state satisfies the expected Navier-Stokes form. It belongs to the ClassicalBridge.Fluids layer that prepares the continuum limit pipeline. Within Recognition Science it contributes to the controlled passage from discrete to continuous descriptions, consistent with the forcing chain that derives spatial dimension and dynamics from the J-functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.