duhamelRemainderOfGalerkin
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 in Recognition Science
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.
scope and limits
- Does not assume the trajectory satisfies the discrete Navier-Stokes ODE.
- Does not derive bounds, convergence, or existence results.
- Does not address 3D flows or non-periodic domains.
- Does not compute numerical values for any specific truncation N.
formal statement (Lean)
344noncomputable def duhamelRemainderOfGalerkin {N : ℕ} (ν : ℝ) (u : ℝ → GalerkinState N) : ℝ → FourierState2D :=
proof body
Definition body.
345 fun t k => (extendByZero (u t) k) - (heatFactor ν t k) • (extendByZero (u 0) k)
346
347/-- If a Galerkin trajectory satisfies the discrete NS ODE, then its Duhamel remainder satisfies a
348forced linear ODE per mode, with forcing `-(extendByZero (B(u,u)))`.
349
350This is the differential version of the Duhamel/variation-of-constants formula. -/