rs_implies_global_regularity_2d_stokesODECoeffBound
plain-language theorem explainer
Under uniform bounds on Galerkin approximants together with modewise convergence to a candidate limit and the assumption that approximants obey the mild Stokes identity, the limit trajectory satisfies the differential Stokes equation per Fourier mode. Researchers closing the 2D continuum limit in the Recognition Science classical bridge would cite this step when converting mild solutions to strong form. The proof is a term-mode wrapper that extracts the limit from ConvergenceHypothesis, inherits the coefficient bound, and converts the mild form
Claim. Let the Galerkin approximants satisfy uniform bounds by constant $B$ and converge modewise to a limit trajectory $u$. Assume further that each extended coefficient obeys the mild identity $u_N(t,k)=e^{-ν|k|^2 t}u_N(0,k)$ for $t≥0$. Then there exists a limit $u:ℝ→FourierState2D$ such that the approximants converge pointwise to $u(t)$ in each mode, the coefficients of $u$ remain bounded by $B$, and $u$ satisfies the differential Stokes equation modewise.
background
The module Regularity2D supplies the top-level composition theorem for the 2D pipeline: Galerkin2D approximations, LNAL semantics, one-step simulation, CPM instantiation, and continuum-limit packaging yield an abstract existence statement without axioms. UniformBoundsHypothesis encodes the uniform bound $B$ on the approximants $u_N$. ConvergenceHypothesis packages a candidate limit trajectory $u:ℝ→FourierState2D$ together with the pointwise Tendsto condition that the zero-extended Galerkin coefficients converge to $u(t)$ in each mode $k$. FourierState2D is the type of all mode-indexed velocity coefficients; extendByZero pads a truncated GalerkinState by zero outside its window. heatFactor($ν,t,k$) is the explicit multiplier $e^{-ν kSq(k) t}$.
proof idea
The term proof refines to the triple consisting of the limit $u$ from ConvergenceHypothesis, the convergence predicate, the inherited bound, and the ODE trajectory. Convergence and the bound are discharged by simpa, the latter via coeff_bound_of_uniformBounds. The trajectory property is obtained by first constructing an IsStokesMildTraj instance from the supplied forall mild identity using stokesMild_of_forall, then applying the conversion lemma IsStokesMildTraj.stokesODE.
why it matters
This theorem supplies the differential Stokes form required by the parent regularity statements rs_implies_global_regularity_2d and its coefficient-bound siblings in the same module. It completes the mild-to-ODE passage inside the M6 composition chain for ClassicalBridge.Fluids, ensuring the continuum limit satisfies the linear evolution without introducing new hypotheses. The result aligns with the Recognition Science program of deriving classical continuum statements from discrete forcing-chain primitives while keeping the dependency graph axiom-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.