rs_implies_global_regularity_2d_stokesMildCoeffBound
Uniform bounds on Galerkin approximants to 2D Stokes flow, combined with modewise convergence to a limit Fourier trajectory and the mild heat identity on each approximant, yield a bounded limit that satisfies the mild Stokes equation. Researchers tracing the Recognition Science classical bridge to Navier-Stokes regularity cite this as the Stokes-mild branch of the 2D pipeline composition. The proof is a direct term-mode wrapper that extracts the limit trajectory, applies the coefficient bound lemma, and transfers the mild identity via stokesMld
claimLet $H$ be a uniform bounds hypothesis on a sequence of Galerkin states $u_N$ and let $C$ be a convergence hypothesis supplying a limit trajectory $u$. For viscosity parameter $ν$ assume that each approximant satisfies the mild identity: for all $N$, $t≥0$ and mode $k$, the zero-extended coefficient equals the heat factor $e^{-ν|k|^2 t}$ times the initial coefficient. Then there exists a limit $u:ℝ→FourierState_{2D}$ such that $u_N(t)$ converges modewise to $u(t)$, the coefficients remain bounded by the uniform bound $B$, and $u$ satisfies the mild Stokes trajectory equation.
background
The module Regularity2D supplies the top-level composition theorem for the 2D pipeline: Galerkin2D approximations plus LNAL semantics plus simulation plus CPM instantiation plus continuum-limit packaging imply an abstract continuum solution. FourierState2D is the type of full (infinite) Fourier coefficient maps from Mode2 to VelCoeff. extendByZero pads a truncated GalerkinState N to this full state by zero outside the truncation window. ConvergenceHypothesis is the structure containing a candidate limit trajectory u together with the statement that the zero-extended Galerkin coefficients converge pointwise to u(t) in the nhds topology. IsStokesMildTraj ν u asserts that for all t≥0 and every mode k the coefficient satisfies (u t) k = heatFactor ν t k • (u 0) k, where heatFactor is the explicit exponential decay e^{-ν|k|^2 t}.
proof idea
The term proof refines the existential goal to the triple consisting of the limit trajectory supplied by the convergence hypothesis, the inherited coefficient bound, and the mild-trajectory property. It applies simpa to discharge the convergence statement directly from Hconv.converges. It invokes coeff_bound_of_uniformBounds on the convergence hypothesis to obtain the uniform bound for every t≥0 and mode k. It finishes by applying stokesMild_of_forall to transfer the assumed mild identity on approximants to the limit trajectory.
why it matters in Recognition Science
This theorem completes the Stokes-mild branch of the 2D regularity pipeline inside the M6 milestone, packaging the continuum limit without a separate IdentificationHypothesis. It feeds the family of rs_implies_global_regularity_2d_* declarations that compose the classical bridge from discrete approximations to an abstract continuum solution. In the Recognition Science framework it supports the derivation of linear fluid equations from the Recognition Composition Law by showing that the mild Stokes form survives the Galerkin-to-continuum passage under the uniform-bounds hypothesis.
scope and limits
- Does not establish regularity for the full nonlinear Navier-Stokes equations.
- Does not address three-dimensional flows.
- Does not remove the uniform bounds hypothesis on the approximants.
- Does not supply an explicit construction of the limit beyond the assumed convergence.
formal statement (Lean)
105theorem rs_implies_global_regularity_2d_stokesMildCoeffBound
106 (Hbounds : UniformBoundsHypothesis)
107 (Hconv : ConvergenceHypothesis Hbounds)
108 (ν : ℝ)
109 (hMild :
110 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
111 (extendByZero (Hbounds.uN N t) k) =
112 (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k)) :
113 ∃ u : ℝ → FourierState2D,
114 (∀ t : ℝ, ∀ k : Mode2,
115 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
116 (nhds ((u t) k)))
117 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
118 ∧ IsStokesMildTraj ν u := by
proof body
Term-mode proof.
119 refine ⟨Hconv.u, ?_, ?_, ?_⟩
120 · simpa using Hconv.converges
121 · intro t ht k
122 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
123 · exact ConvergenceHypothesis.stokesMild_of_forall (HC := Hconv) (ν := ν) hMild
124
125/-- Same as `rs_implies_global_regularity_2d_stokesMildCoeffBound`, but returns the **differential**
126(within `t ≥ 0`) Stokes/heat equation per mode.
127
128This is derived from the mild identity via `IsStokesMildTraj.stokesODE`. -/