galerkinNS_hasDerivAt_extendByZero_mode
plain-language theorem explainer
If a Galerkin trajectory satisfies the projected Navier-Stokes ODE, then its zero-extension to the full Fourier coefficient space obeys the corresponding modewise linear evolution at each retained mode. Analysts constructing spectral approximations to 2D incompressible flow would cite the result when passing from finite-dimensional Galerkin systems to continuum Fourier states. The argument applies the differentiation-through-extension lemma and rewrites the right-hand side by linearity of extendByZero together with the explicit Laplacian-coeffi
Claim. Let $u : ℝ → GalerkinState_N$ satisfy $u'(t) = ν Δ u(t) - B(u(t), u(t))$ in the Galerkin sense. Then for each mode $k$, the map $s ↦ [extendByZero(u(s))]_k$ is differentiable at $t$ with derivative $ν (-|k|^2) [extendByZero(u(t))]_k - [extendByZero(B(u(t), u(t)))]_k$.
background
The module ContinuumLimit2D builds a Lean pipeline from finite Galerkin approximations of 2D Navier-Stokes to an infinite Fourier coefficient state. The embedding extendByZero pads a GalerkinState N with zeros outside the retained modes, producing an element of FourierState2D. Its linearity is recorded in extendByZero_add, extendByZero_smul and extendByZero_neg; the action on the Laplacian appears in extendByZero_laplacianCoeff. The upstream lemma hasDerivAt_extendByZero_apply supplies the generic rule that differentiation commutes with this zero-extension when the derivative is taken in the Galerkin space.
proof idea
The proof first invokes hasDerivAt_extendByZero_apply on the Galerkin right-hand side to obtain the derivative of the extended function. It then applies simp using extendByZero_smul, extendByZero_add, extendByZero_neg and extendByZero_laplacianCoeff to replace the extended Galerkin RHS by the explicit viscous term minus the extended convection term, after which simpa closes the goal.
why it matters
This result is used directly by galerkinNS_hasDerivAt_duhamelRemainder_mode to derive the forced linear ODE satisfied by the Duhamel remainder of a Galerkin trajectory. It forms part of the differential bridge inside the M5 milestone of ContinuumLimit2D, which prepares the ground for integrating to the variation-of-constants formula. Within the Recognition Science framework the construction supplies a rigorous classical limit step that can later be connected to the phi-ladder and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.