IndisputableMonolith.NavierStokes.GalerkinEquicontinuity
This module supplies equicontinuity tools for the Galerkin truncations of 3D Navier-Stokes on the torus. It would be cited in compactness arguments that pass to the limit in the approximating sequence. The structure relies on McShane Lipschitz extensions combined with density of the rationals to produce a uniform modulus of continuity in time.
claimThe family of Galerkin solutions $u_N$ on $T^3$ satisfies: for every $T>0$ and every sequence $t_k,s_k$ with $|t_k-s_k|→0$, one has $||u_N(t_k)-u_N(s_k)||_{L^2}→0$ uniformly in the truncation level $N$.
background
The setting is the 3D spectral Galerkin truncation introduced in the upstream module Galerkin3D: Fourier modes restricted to the cube $[-N,N]^3$ on the torus, with the projected Navier-Stokes system. That module records the energy identity arising from skew-symmetry of the bilinear term $B(u,u)$ and the non-positive dissipation coming from the Laplacian. The present module adds the auxiliary analytic machinery needed to upgrade the $L^2$ energy bound into time equicontinuity.
proof idea
The module is a collection of supporting lemmas rather than a single long proof. It first constructs a Lipschitz constant for the solution map, proves non-negativity, invokes the density of rationals via exists_rat_near, applies the McShane extension theorem on a dense subset, and finally assembles the dense extension to obtain the equicontinuity statement.
why it matters in Recognition Science
These lemmas close the analytic gap between the energy estimates supplied by Galerkin3D and the compactness required for weak solutions of the Navier-Stokes equations. They feed directly into any subsequent global existence argument that extracts a limit from the Galerkin sequence via Arzelà-Ascoli or Aubin-Lions.
scope and limits
- Does not establish existence or uniqueness of solutions.
- Does not improve spatial regularity beyond the Galerkin level.
- Does not treat the inviscid Euler limit.
- Does not supply explicit numerical values for the modulus of continuity.