duhamelRemainderOfGalerkin
plain-language theorem explainer
The Duhamel remainder for a Galerkin trajectory in 2D is defined modewise in Fourier space as the difference between the zero-extended current coefficient and the heat-evolved initial coefficient. Analysts deriving integral forms of the discrete Navier-Stokes ODE cite this when passing from finite-dimensional systems to continuum limits. The definition is a direct pointwise subtraction using the zero-extension embedding and the exponential heat multiplier.
Claim. $R(t,k) := E(u(t))(k) - e^{-ν |k|^2 t} E(u(0))(k)$, where $E$ is the zero-extension map from the truncated Galerkin state (Euclidean space over modes $N$ times two components) to the full Fourier coefficient state (functions from Mode2 to velocity coefficients) and the exponential is the heat factor.
background
The module ContinuumLimit2D sets up a Lean-checkable pipeline from finite Galerkin approximations to a continuum Fourier object for 2D fluids on the torus. FourierState2D is the type of all mode coefficients Mode2 → VelCoeff. GalerkinState N is the finite-dimensional Euclidean space of coefficients on the truncated modes N times Fin 2. extendByZero pads a GalerkinState by zero outside its window. heatFactor ν t k returns the real exponential exp(-ν kSq(k) t), the modewise Stokes decay factor.
proof idea
One-line definition that subtracts the heat-evolved initial extended state from the current extended state at each time t and mode k, using the sibling definitions extendByZero and heatFactor.
why it matters
This definition is invoked by duhamelRemainderOfGalerkin_integratingFactor and duhamelRemainderOfGalerkin_kernel, which produce the integral Duhamel identity galerkin_duhamelKernel_identity. It supplies the explicit remainder term needed for the variation-of-constants formula on each Fourier mode, closing one step in the Milestone M5 pipeline from discrete ODE to continuum limit. The construction stays inside the classical fluids bridge and does not yet invoke Recognition Science forcing landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.