rs_implies_global_regularity_2d_nsDuhamelCoeffBound
plain-language theorem explainer
The theorem shows that if Galerkin approximants remain uniformly bounded and converge modewise to a limit Fourier trajectory u while satisfying a Duhamel identity with remainders D_N converging to D, then u obeys the nonlinear Stokes-Duhamel trajectory equation. Researchers closing the continuum limit for 2D Navier-Stokes regularity in the Recognition Science pipeline would cite this result. The proof is a direct term construction that extracts the limit u from the convergence hypothesis and applies the nsDuhamel passage lemma.
Claim. Suppose the Galerkin approximants satisfy uniform bounds by $B$ and converge modewise to a limit trajectory $u$. Assume the approximants obey the identity $u_N(t,k) = e^{-ν|k|^2 t} u_N(0,k) + D_N(t,k)$ with $D_N$ converging modewise to $D$. Then there exists a limit $u$ such that the coefficients converge, remain bounded by $B$, and $u$ satisfies the nonlinear Duhamel trajectory equation IsNSDuhamelTraj($ν$, $D$, $u$).
background
The Regularity2D module composes the 2D fluid pipeline: Galerkin approximations, LNAL semantics, simulation, CPM instantiation, and continuum-limit packaging to obtain an abstract existence statement for continuum solutions without axioms or sorrys. FourierState2D denotes the space of all mode-indexed velocity coefficients on the torus; extendByZero pads a truncated Galerkin state with zeros outside its window. heatFactor is the modewise multiplier $e^{-ν|k|^2 t}$ that encodes the linear Stokes/heat evolution.
proof idea
The term proof refines the goal to the triple consisting of the candidate limit trajectory, the inherited coefficient bound, and the Duhamel property. Convergence of coefficients is transferred directly by simpa from the hypothesis. The bound is obtained by applying coeff_bound_of_uniformBounds to the convergence hypothesis. The nonlinear trajectory property IsNSDuhamelTraj is supplied exactly by nsDuhamel_of_forall, which passes the approximant identity to the limit.
why it matters
This declaration supplies the Duhamel-style remainder identity required by the top-level 2D regularity composition theorem. It feeds the parent claim rs_implies_global_regularity_2d by packaging the nonlinear term in the continuum limit. Within the Recognition Science framework it closes one step of the classical-bridge pipeline, showing how discrete φ-ladder approximations yield continuum trajectories consistent with the eight-tick octave and self-similar fixed-point structure, though specialized here to two spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.