rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp
plain-language theorem explainer
This theorem delivers the existence of a limit Fourier trajectory satisfying the 2D Navier-Stokes Duhamel integral equation when the forcing satisfies a concrete Galerkin dominated-convergence hypothesis. Workers on the Recognition Science 2D regularity pipeline cite it to instantiate the abstract convergence result with explicit Galerkin data. The proof is a one-line wrapper that invokes the general forcing version and supplies the required dominated-convergence datum via GalerkinForcingDominatedConvergenceHypothesis.forcingDCTAt.
Claim. Let $H$ be a uniform bounds hypothesis on Galerkin approximants $u_N$, let $H_c$ be a convergence hypothesis to a candidate limit, let $0 ≤ ν$, let $B_N$ be convection operators, and assume each $u_N$ satisfies the Galerkin Navier-Stokes ODE, the Duhamel integrands are interval-integrable, and the Galerkin forcing obeys the dominated-convergence hypothesis. Then there exists a trajectory $u:ℝ→$FourierState$_{2D}$ such that $u_N(t)$ converges pointwise to $u(t)$ modewise, $‖u(t)‖≤B$, and $u$ equals the Duhamel integral of the forcing with kernel $duhamelKernelIntegral(ν,F)$.
background
The Regularity2D module composes the 2D pipeline (Galerkin2D + LNAL semantics + simulation + CPM + continuum limit) into an abstract existence statement without axioms or sorry. FourierState2D is the space of all mode-to-coefficient maps on the torus; extendByZero pads a truncated GalerkinState$N$ by zero outside its window. duhamelKernelIntegral(ν,F) is the operator sending $(t,k)$ to $-∫_0^t$ heatFactor(ν,t-s,k)·F(s,k) ds. ConvergenceHypothesis packages a candidate limit trajectory together with pointwise modewise convergence of the extended approximants. GalerkinForcingDominatedConvergenceHypothesis supplies a concrete forcing trajectory F together with the dominated-convergence data needed for the integral to pass to the limit.
proof idea
One-line wrapper that applies rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing after extracting the forcing term. The single tactic step intro t ht k followed by simpa [galerkinForcing] using GalerkinForcingDominatedConvergenceHypothesis.forcingDCTAt supplies the ForcingDominatedConvergenceAt instance required by the callee.
why it matters
The declaration completes the concrete forcing case inside the M6 composition theorem for 2D Navier-Stokes regularity. It is used by the top-level rs_implies_global_regularity_2d to obtain an IsNSDuhamelTraj limit under Galerkin data. Within the Recognition framework it realises the continuum-limit step of the forcing chain, converting discrete convection operators into a Duhamel trajectory while preserving the uniform bound B; the 2D case serves as the first non-trivial test before any 3D extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.