rs_implies_global_regularity_2d_stokesODECoeffBound
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
claimLet 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 in Recognition Science
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.
scope and limits
- Does not establish the uniform bounds or convergence hypotheses themselves.
- Does not treat the nonlinear Navier-Stokes terms.
- Does not extend to three spatial dimensions.
- Does not supply convergence rates or explicit error bounds.
- Does not address domains other than the flat torus.
formal statement (Lean)
129theorem rs_implies_global_regularity_2d_stokesODECoeffBound
130 (Hbounds : UniformBoundsHypothesis)
131 (Hconv : ConvergenceHypothesis Hbounds)
132 (ν : ℝ)
133 (hMild :
134 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
135 (extendByZero (Hbounds.uN N t) k) =
136 (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k)) :
137 ∃ u : ℝ → FourierState2D,
138 (∀ t : ℝ, ∀ k : Mode2,
139 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
140 (nhds ((u t) k)))
141 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
142 ∧ IsStokesODETraj ν u := by
proof body
Term-mode proof.
143 refine ⟨Hconv.u, ?_, ?_, ?_⟩
144 · simpa using Hconv.converges
145 · intro t ht k
146 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
147 ·
148 have hm : IsStokesMildTraj ν Hconv.u :=
149 ConvergenceHypothesis.stokesMild_of_forall (HC := Hconv) (ν := ν) hMild
150 exact IsStokesMildTraj.stokesODE hm
151
152/-- Variant of the top-level theorem returning a first nonlinear (Duhamel-style) remainder identity.
153
154This uses `ConvergenceHypothesis.nsDuhamel_of_forall` to pass the identity to the limit,
155assuming the approximants satisfy the identity with remainders `D_N` that converge modewise. -/