nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp
plain-language theorem explainer
This definition constructs the IdentificationHypothesis for a ConvergenceHypothesis by packaging uniform bounds on Galerkin trajectories, a limit Fourier state, the Galerkin Navier-Stokes derivative condition, integrability of extended forcing terms, and a dominated convergence hypothesis on the Galerkin forcing. Analysts formalizing the passage from finite-dimensional 2D approximations to continuum Navier-Stokes solutions cite it to instantiate the forcing identification step with concrete data. The construction is a one-line wrapper that dis-
Claim. Let $H$ be a uniform bounds hypothesis on a family of Galerkin trajectories $u_N$. Given a convergence hypothesis $HC$ supplying a candidate limit trajectory $u$, viscosity parameter $ν ≥ 0$, convection operators $B_{op}$, the assumption that each $u_N$ satisfies the time derivative of the Galerkin Navier-Stokes right-hand side, interval integrability of the extended convection terms, and a Galerkin forcing dominated convergence hypothesis $hForce$ providing a limit forcing $F$ together with an integrable dominating function, the definition yields the identification hypothesis for $HC$.
background
The module ContinuumLimit2D (Milestone M5) defines a Lean-checkable pipeline shape for passing from finite-dimensional 2D Galerkin approximations to a continuum limit object, keeping hypotheses explicit so later work can replace them with proofs. UniformBoundsHypothesis packages a family of Galerkin trajectories $u_N$ together with a uniform bound $B$ such that $‖u_N(t)‖ ≤ B$ for all $N$ and $t ≥ 0$. ConvergenceHypothesis supplies a candidate limit $u : ℝ → FourierState2D$ and asserts pointwise mode-by-mode convergence of the zero-extended Galerkin coefficients. GalerkinForcingDominatedConvergenceHypothesis supplies a limit forcing $F$, an integrable dominating bound, and measurability data for the family $F_N = galerkinForcing H B_{op}$. Upstream, forcingDCTAt converts the concrete dominated-convergence hypothesis into the abstract ForcingDominatedConvergenceAt datum required by the more general identification lemma.
proof idea
The definition is a one-line wrapper that applies nsDuhamelCoeffBound_galerkinKernel_of_forcing after setting the forcing field to the $F$ component of the Galerkin forcing dominated convergence hypothesis. The remaining argument is supplied by a short intro block that invokes GalerkinForcingDominatedConvergenceHypothesis.forcingDCTAt and simplifies via the definition of galerkinForcing.
why it matters
This declaration supplies the concrete forcing identification step inside the explicit hypothesis pipeline of Milestone M5. It feeds the milestone theorem that combines uniform bounds, convergence, and identification to obtain a packaged continuum solution. By instantiating the abstract forcing hypothesis with GalerkinForcingDominatedConvergenceHypothesis it makes the dependency graph for the classical bridge explicit, allowing later replacement of the hypothesis by a proof. The construction stays within the 2D Fourier setting and does not invoke Recognition Science landmarks such as the forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.