rs_implies_global_regularity_2d_coeffBound
plain-language theorem explainer
Uniform bounds on Galerkin approximants for 2D Navier-Stokes, paired with a convergence hypothesis, produce a limit Fourier trajectory whose mode coefficients converge from the approximants and stay bounded by the same constant B for all nonnegative times. Researchers closing the 2D regularity argument inside the Recognition Science classical bridge would cite this variant to bypass a separate identification hypothesis. The proof is a direct term construction that selects the limit object from the convergence hypothesis and invokes the closed-b
Claim. Let $H$ be a uniform bounds hypothesis on the Galerkin approximants $u_N$. Let $C$ be a convergence hypothesis relative to $H$. Then there exists a map $u :$ reals to Fourier coefficient states such that for every real $t$ and mode $k$ the zero-extended coefficients of $u_N(t)$ converge to those of $u(t)$ as truncation tends to infinity, and moreover the coefficients of $u(t)$ satisfy the bound $B$ from $H$ for all $t$ at least zero.
background
The Regularity2D module composes the 2D fluid pipeline from Galerkin approximations through LNAL semantics, one-step simulation, CPM instantiation and continuum-limit packaging into an abstract existence statement. UniformBoundsHypothesis asserts that all Galerkin coefficients remain inside a fixed ball of radius $B$ uniformly in time and truncation level. ConvergenceHypothesis supplies a candidate limit trajectory $u$ together with modewise convergence of the zero-extended approximants. The upstream lemma coeff_bound_of_uniformBounds records that uniform boundedness of the approximants passes to the limit coefficients by closedness of the metric ball.
proof idea
The proof is a term-mode wrapper. It refines the existential by taking the limit trajectory directly from the convergence hypothesis. The convergence conjunct is discharged by simplification of the convergence field. The bound conjunct is obtained by applying the coefficient bound lemma to the convergence hypothesis at each nonnegative time and mode.
why it matters
This theorem supplies a minimal form of the global regularity claim for 2D flows by deriving the coefficient bound directly from uniform bounds and convergence, without a separate IdentificationHypothesis. It supports the top-level composition theorem in Regularity2D that packages the full pipeline from Galerkin2D through ContinuumLimit2D. The construction keeps the identification step abstract, consistent with the Recognition Science forcing chain at the classical-bridge stage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.