rs_implies_global_regularity_2d_divFreeCoeffBound
plain-language theorem explainer
This theorem establishes that uniform bounds on 2D Galerkin approximants, together with modewise convergence to a limit Fourier trajectory and the assumption that each approximant is divergence-free in Fourier space, yield a bounded divergence-free limit trajectory. Researchers composing the Recognition Science 2D fluid pipeline would cite it as a self-contained variant of the global regularity statement that derives the coefficient bound and divergence-free property internally. The proof is a direct term-mode extraction that pulls the limit u,
Claim. Let $H$ be a uniform bounds hypothesis on the Galerkin approximants $u_N$ with bound $B$. Let $C$ be a convergence hypothesis for $H$ supplying a candidate limit trajectory $u$. Assume that for every $N$, $t$, and 2D Fourier mode $k$ the zero-extended approximant satisfies the Fourier divergence constraint. Then there exists a trajectory $u$ such that the approximants converge modewise to $u(t,k)$, the coefficients of $u$ remain bounded by $B$ for all $t≥0$, and $u$ is divergence-free.
background
The module Regularity2D supplies the top-level composition theorem for the 2D pipeline: Galerkin2D approximants plus LNAL semantics plus simulation plus CPM plus continuum-limit packaging imply an abstract continuum solution. Key supporting definitions appear in ContinuumLimit2D. UniformBoundsHypothesis packages a family of Galerkin states $u_N$ together with a uniform bound $B$ on their coefficients. ConvergenceHypothesis $C$ for such an $H$ supplies a candidate limit map $u:ℝ→FourierState2D$ and the statement that, for every time $t$ and mode $k$, the zero-extended coefficients of $u_N(t)$ converge to those of $u(t)$ in the natural topology. The auxiliary function extendByZero pads a truncated Galerkin state to a full Fourier coefficient vector. The predicate divConstraint $k(v)$ extracts the Fourier-side divergence of a velocity coefficient $v$ at mode $k$. The predicate IsDivergenceFreeTraj asserts that the trajectory satisfies the divergence constraint at every time and mode.
proof idea
The proof is a one-line term-mode wrapper. It constructs the triple by taking the limit trajectory $u$ supplied by the convergence hypothesis, then applies the convergence statement directly for the first conjunct. The second conjunct (coefficient bound) is obtained by invoking coeff_bound_of_uniformBounds on the convergence hypothesis. The third conjunct (divergence-free trajectory) is obtained by invoking divFree_of_forall on the convergence hypothesis together with the supplied forall-divergence assumption.
why it matters
This declaration is one of several variants of the top-level regularity theorem rs_implies_global_regularity_2d in the ClassicalBridge.Fluids module. It closes the 2D pipeline composition (M1–M5) by deriving both the coefficient bound and the divergence-free property from the convergence hypothesis, thereby avoiding a separate IdentificationHypothesis. In the Recognition Science framework it supplies a concrete existence statement for a divergence-free continuum limit under the uniform-bounds and convergence assumptions that are themselves obtained from the Galerkin and CPM stages. No downstream uses are recorded yet; the result therefore functions as an internal milestone rather than a lemma invoked elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.