nsDuhamelCoeffBound_galerkinKernel_of_forcing
plain-language theorem explainer
This definition constructs an identification hypothesis for the continuum limit of 2D Galerkin Navier-Stokes approximations when dominated convergence is assumed directly on the forcing terms. Analysts deriving rigorous continuum limits from finite truncations cite it to close the Duhamel representation step. The construction defines the extended forcing family from the convection operators and reduces the problem to a kernel-integral bound via the Galerkin Duhamel identity lemma.
Claim. Let $H$ be a uniform bounds hypothesis on Galerkin trajectories $u_N$ and let $HC$ be the associated convergence hypothesis to a limit trajectory $u$. For viscosity parameter $ν ≥ 0$, convection operators $B_N$, and trajectories satisfying the time derivative condition with right-hand side given by the Galerkin Navier-Stokes operator, together with interval integrability of the extended forcing terms and forcing-dominated convergence of the approximants to a limit forcing $F$, the identification hypothesis for $HC$ holds.
background
The module ContinuumLimit2D develops a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum Fourier coefficient state. Key objects include the uniform bounds hypothesis, a structure asserting that a family of Galerkin trajectories $u_N(t)$ remains bounded by a constant $B$ independent of truncation level $N$ for all $t ≥ 0$. The convergence hypothesis assumes the existence of a limit trajectory $u(t)$ in the full Fourier state such that the zero-extended Galerkin coefficients converge pointwise to those of $u$ via the extend-by-zero map. The Duhamel kernel integral applies the heat kernel factor to a forcing trajectory. Forcing-dominated convergence at a fixed time and mode supplies a bound and measurability ensuring the forcing approximants converge under the dominated convergence theorem, which implies the corresponding kernel integrand convergence when $ν ≥ 0$.
proof idea
The proof first defines the forcing family $F_N$ by extending the convection term $B_N(u_N(s), u_N(s))$. It then invokes the Galerkin Duhamel kernel identity to establish that each approximant satisfies the integral equation with the heat factor and the Duhamel integral of $F_N$. Finally it applies the kernel-integral version of the coefficient bound constructor, passing the forcing-dominated convergence hypothesis directly.
why it matters
This definition supplies the forcing-level variant of the Duhamel coefficient bound needed to identify the limit in the continuum pipeline. It is invoked by the concrete hypothesis version that packages the Galerkin forcing convergence. Within the Recognition Science framework it advances the classical bridge milestone by making the analytic identification step explicit and hypothesis-driven, consistent with the overall program of deriving continuum physics from discrete structures without hidden axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.