rs_implies_global_regularity_2d_nsDuhamelCoeffBound
The theorem shows that if Galerkin approximants remain uniformly bounded and converge modewise to a limit Fourier trajectory u while satisfying a Duhamel identity with remainders D_N converging to D, then u obeys the nonlinear Stokes-Duhamel trajectory equation. Researchers closing the continuum limit for 2D Navier-Stokes regularity in the Recognition Science pipeline would cite this result. The proof is a direct term construction that extracts the limit u from the convergence hypothesis and applies the nsDuhamel passage lemma.
claimSuppose the Galerkin approximants satisfy uniform bounds by $B$ and converge modewise to a limit trajectory $u$. Assume the approximants obey the identity $u_N(t,k) = e^{-ν|k|^2 t} u_N(0,k) + D_N(t,k)$ with $D_N$ converging modewise to $D$. Then there exists a limit $u$ such that the coefficients converge, remain bounded by $B$, and $u$ satisfies the nonlinear Duhamel trajectory equation IsNSDuhamelTraj($ν$, $D$, $u$).
background
The Regularity2D module composes the 2D fluid pipeline: Galerkin approximations, LNAL semantics, simulation, CPM instantiation, and continuum-limit packaging to obtain an abstract existence statement for continuum solutions without axioms or sorrys. FourierState2D denotes the space of all mode-indexed velocity coefficients on the torus; extendByZero pads a truncated Galerkin state with zeros outside its window. heatFactor is the modewise multiplier $e^{-ν|k|^2 t}$ that encodes the linear Stokes/heat evolution.
proof idea
The term proof refines the goal to the triple consisting of the candidate limit trajectory, the inherited coefficient bound, and the Duhamel property. Convergence of coefficients is transferred directly by simpa from the hypothesis. The bound is obtained by applying coeff_bound_of_uniformBounds to the convergence hypothesis. The nonlinear trajectory property IsNSDuhamelTraj is supplied exactly by nsDuhamel_of_forall, which passes the approximant identity to the limit.
why it matters in Recognition Science
This declaration supplies the Duhamel-style remainder identity required by the top-level 2D regularity composition theorem. It feeds the parent claim rs_implies_global_regularity_2d by packaging the nonlinear term in the continuum limit. Within the Recognition Science framework it closes one step of the classical-bridge pipeline, showing how discrete φ-ladder approximations yield continuum trajectories consistent with the eight-tick octave and self-similar fixed-point structure, though specialized here to two spatial dimensions.
scope and limits
- Does not establish the uniform bounds hypothesis on the approximants.
- Does not treat the three-dimensional Navier-Stokes system.
- Does not supply convergence rates or quantitative estimates.
- Does not address domains other than the flat torus.
formal statement (Lean)
156theorem rs_implies_global_regularity_2d_nsDuhamelCoeffBound
157 (Hbounds : UniformBoundsHypothesis)
158 (Hconv : ConvergenceHypothesis Hbounds)
159 (ν : ℝ)
160 (D_N : ℕ → ℝ → FourierState2D) (D : ℝ → FourierState2D)
161 (hD : ∀ t : ℝ, ∀ k : Mode2,
162 Filter.Tendsto (fun N : ℕ => (D_N N t) k) Filter.atTop (nhds ((D t) k)))
163 (hId :
164 ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
165 (extendByZero (Hbounds.uN N t) k) =
166 (heatFactor ν t k) • (extendByZero (Hbounds.uN N 0) k) + (D_N N t) k) :
167 ∃ u : ℝ → FourierState2D,
168 (∀ t : ℝ, ∀ k : Mode2,
169 Filter.Tendsto (fun N : ℕ => (extendByZero (Hbounds.uN N t)) k) Filter.atTop
170 (nhds ((u t) k)))
171 ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ Hbounds.B)
172 ∧ IsNSDuhamelTraj ν D u := by
proof body
Term-mode proof.
173 refine ⟨Hconv.u, ?_, ?_, ?_⟩
174 · simpa using Hconv.converges
175 · intro t ht k
176 simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := Hconv) t ht k)
177 ·
178 -- Pass the Duhamel-style identity to the limit.
179 exact ConvergenceHypothesis.nsDuhamel_of_forall (HC := Hconv) (ν := ν) (D_N := D_N) (D := D) hD hId
180
181/-- Variant of the top-level theorem returning a first nonlinear (Duhamel-style) remainder identity,
182where the remainder is produced from the **Galerkin nonlinearity** via the Duhamel kernel integral.
183
184This removes the need to provide `D_N`, `D`, and the approximation identity explicitly; the only
185missing analytic ingredient is the dominated-convergence hypothesis `hDC` for the kernel integrands. -/