stokesMild_of_forall
plain-language theorem explainer
The theorem shows that the mild Stokes/heat identity passes to the modewise limit trajectory whenever every Galerkin approximant satisfies the same identity. Researchers constructing rigorous continuum limits for 2D viscous flows would cite it when identifying the limit object. The argument extracts modewise convergence at fixed t and k, transports the initial data through continuous scalar multiplication by the heat factor, and concludes equality by uniqueness of limits once the sequences agree for all N.
Claim. Let $H$ be a uniform bounds hypothesis supplying a family of Galerkin trajectories $u_N$ and let $HC$ be the associated convergence hypothesis with candidate limit trajectory $u$. For viscosity parameter $ν$, suppose that for every truncation level $N$, every $t≥0$ and every mode $k$ the zero-extended coefficient satisfies $extendByZero(u_N(N,t),k)=(heatFactor ν t k)·extendByZero(u_N(N,0),k)$. Then the limit trajectory satisfies the mild Stokes equation: for all $t≥0$ and modes $k$, $u(t,k)=(heatFactor ν t k)·u(0,k)$.
background
The ContinuumLimit2D module (milestone M5) packages the passage from finite-dimensional Galerkin approximations to a continuum Fourier trajectory as an explicit pipeline of hypotheses. A UniformBoundsHypothesis consists of a family of Galerkin trajectories $uN$ together with a uniform bound $B$ such that $‖uN N t‖≤B$ for all $N$ and $t≥0$. The ConvergenceHypothesis built on top of it supplies a limit map $u:ℝ→FourierState2D$ and asserts modewise convergence of the zero-extended Galerkin coefficients to the corresponding coefficients of $u$.
proof idea
The proof fixes arbitrary $t≥0$ and mode $k$. It obtains convergence of the extended coefficients at time $t$ and at time $0$ directly from the convergence hypothesis. Continuity of scalar multiplication by the constant heatFactor $ν t k$ transports the time-zero convergence to a convergence statement for the multiplied sequence. The mild hypothesis on the approximants yields that the two sequences agree for every $N$, hence are eventually equal. Uniqueness of limits in a Hausdorff space then forces the desired equality for the limit trajectory.
why it matters
The result supplies the mild Stokes identity inside the identification constructor stokesMildCoeffBound, which is invoked by the regularity theorems rs_implies_global_regularity_2d_stokesMildCoeffBound and rs_implies_global_regularity_2d_stokesODECoeffBound in Regularity2D. It therefore closes one explicit step of the M5 pipeline that replaces Galerkin approximants by a continuum object while keeping every identification hypothesis visible. Within the Recognition Science framework it contributes to the classical bridge by showing how linear evolution identities survive the continuum limit under the stated modewise convergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.