rs_implies_global_regularity_2d_coeffBound
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish that the limit satisfies the Navier-Stokes equations.
- Does not extend to three-dimensional flows or non-periodic domains.
- Does not supply convergence rates or stability estimates.
- Does not incorporate external forcing or variable viscosity.
formal statement (Lean)
60theorem rs_implies_global_regularity_2d_coeffBound
61 (Hbounds : UniformBoundsHypothesis)
62 (Hconv : ConvergenceHypothesis Hbounds) :
63 ∃ u : ℝ → FourierState2D,
64 (∀ t : ℝ, ∀ k : Mode2,
65 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
66 (nhds ((u t) k)))
67 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B) := by
proof body
Term-mode proof.
68 -- Take the limit object from convergence, and use the derived bound lemma.
69 refine ⟨Hconv.u, ?_, ?_⟩
70 · simpa using Hconv.converges
71 · intro t ht k
72 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
73
74/-- Variant of the top-level theorem where the derived “identification” is:
75
76- the **proved** coefficient bound (from uniform bounds + convergence), and
77- the **proved** divergence-free constraint (passed to the limit under modewise convergence),
78 assuming each approximant is divergence-free in Fourier variables.
79
80This avoids providing a separate `IdentificationHypothesis`. -/