duhamelRemainderOfGalerkin_integratingFactor
plain-language theorem explainer
The theorem establishes the integrating-factor form of the Duhamel formula for the modewise remainder of a Galerkin trajectory satisfying the projected 2D Navier-Stokes ODE. Researchers constructing rigorous continuum limits from finite-dimensional fluid models would cite this identity when converting the remainder ODE into an integral equation. The proof defines an auxiliary product G of the exponential factor and the remainder, verifies via the product rule and cancellation that its derivative equals the negative forcing term, and integrates.
Claim. Let $R(t,k)$ denote the Duhamel remainder $R(t,k) := û(t,k) - e^{-ν |k|^2 t} û(0,k)$ obtained by extending a Galerkin state $u$ to Fourier coefficients. Assume the trajectory $u$ satisfies the projected Navier-Stokes ODE at every instant and that the convection forcing term is interval-integrable on $[0,t]$. Then $e^{-ν |k|^2 t} R(t,k) = -∫_0^t e^{-ν |k|^2 s} F(s,k) ds$, where $F(s,k)$ is the $k$-mode of the extended convection operator applied to the pair $(u(s),u(s))$.
background
The ContinuumLimit2D module constructs a Lean-checkable pipeline from finite Galerkin approximations of the 2D Navier-Stokes equations to a continuum Fourier state, keeping analytic compactness steps as explicit hypotheses. The Duhamel remainder is defined by $R(t,k) := extendByZero(u t) k - heatFactor(ν,t,k) • extendByZero(u 0) k$, where heatFactor(ν,t,k) = exp(-ν kSq(k) t) supplies the linear Stokes decay. The upstream theorem galerkinNS_hasDerivAt_duhamelRemainder_mode states that if u satisfies the discrete ODE then the remainder obeys the forced linear ODE ∂_t R = ν(-kSq(k)) R - F(t,k) with forcing F drawn from the convection operator B.
proof idea
The proof proceeds in tactic mode. It introduces the integrating factor E(s) = exp(-a s) with a = ν(-kSq k), the remainder function R, the forcing F, and the product G = E • R. It establishes the derivative of E by composition with the exponential, invokes galerkinNS_hasDerivAt_duhamelRemainder_mode to obtain the derivative of R, and computes the derivative of G to show that the linear terms cancel, leaving -E • F. The integrability hypothesis is transferred to the negative forcing term, intervalIntegral.integral_eq_sub_of_hasDerivAt yields G(t) - G(0), and the initial condition R(0) = 0 (from the definition of the remainder) produces the stated identity after rearrangement.
why it matters
This identity is the immediate predecessor of duhamelRemainderOfGalerkin_kernel, which algebraically rewrites the result into the standard Duhamel kernel form R(t,k) = -∫_0^t heatFactor(ν,t-s,k) • F(s,k) ds. It belongs to the M5 milestone of ContinuumLimit2D, whose module documentation emphasizes making the dependency graph explicit so that later steps can replace hypotheses with proofs. Within the Recognition Science framework the construction supplies the integral representation needed for the classical fluid bridge, though the file itself remains inside the classical setting and does not yet invoke the Recognition Composition Law or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.