rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing
plain-language theorem explainer
This theorem shows that uniform bounds on 2D Galerkin approximants together with pointwise convergence and a dominated-convergence condition only on the forcing term imply that the limit trajectory satisfies the Navier-Stokes Duhamel integral equation. Researchers closing the Recognition Science classical-bridge pipeline from discrete simulations to continuum solutions would cite it. The proof extracts the candidate limit from the convergence hypothesis, verifies the Duhamel identity on approximants via galerkin_duhamelKernel_identity, and dis-
Claim. Let $H$ be a uniform-bounds hypothesis on the Galerkin states $u_N$, let $H_c$ be the associated convergence hypothesis supplying a limit trajectory $u$, let $ν ≥ 0$ be the viscosity, and let $B_N$ be the family of convection operators. Assume the right-hand side satisfies the given derivative condition and the interval-integrability hypothesis. Suppose the forcing trajectory $F$ obeys the ForcingDominatedConvergenceAt condition with respect to the extended convection terms. Then there exists a trajectory $u : ℝ → FourierState_{2D}$ such that the extended Galerkin coefficients converge modewise to $u(t)$, $‖u(t)_k‖ ≤ B$ for all $t ≥ 0$ and all modes $k$, and $u$ satisfies the Duhamel trajectory equation driven by the kernel integral of $F$.
background
The Regularity2D module supplies the top-level composition theorem for the 2D pipeline: Galerkin2D approximations plus LNAL semantics plus one-step simulation plus CPM instantiation plus continuum-limit packaging yield an abstract continuum solution. FourierState2D is the space of all mode coefficients Mode2 → VelCoeff. extendByZero pads a truncated GalerkinState N to a full FourierState2D by zero outside the retained modes. duhamelKernelIntegral ν F (t,k) equals the integral from 0 to t of -heatFactor ν (t-s) k • F(s,k) ds. ConvergenceHypothesis H packages a candidate limit trajectory together with the statement that the zero-extended Galerkin coefficients converge pointwise to it. ForcingDominatedConvergenceAt supplies a dominating function for the forcing alone; under ν ≥ 0 this implies the full kernel dominated-convergence condition because |heatFactor ν (t-s) k| ≤ 1 on the integration interval.
proof idea
The tactic proof enters classical mode and refines the goal to the triple consisting of the limit trajectory from Hconv, the coefficient bound, and the Duhamel trajectory property. Convergence and the bound are discharged by direct simplification using the fields of ConvergenceHypothesis and the upstream lemma coeff_bound_of_uniformBounds. An auxiliary F_N is defined as the extended convection term; the identity relating each approximant to the heat kernel plus Duhamel integral is obtained by applying galerkin_duhamelKernel_identity; the forcing convergence hypothesis is rewritten for F_N by simplification; finally nsDuhamel_of_forall_kernelIntegral_of_forcing is invoked on these data.
why it matters
The declaration belongs to the M6 milestone that composes the entire 2D regularity pipeline without sorries. It directly supplies the forcing-only variant used by the sibling theorem rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp. Within the Recognition Science framework it closes one step of the classical bridge that links discrete recognition steps to continuum Navier-Stokes solutions, supporting the claim that global regularity holds in two dimensions under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.