viscous_norm_bound3
plain-language theorem explainer
The theorem shows that any differentiable curve u(t) in the 3D Galerkin space satisfying the truncated Navier-Stokes ODE has non-increasing Euclidean norm for nonnegative viscosity, provided the convection operator obeys energy skew-symmetry. Researchers on spectral methods for incompressible flow cite it to obtain uniform L2 bounds on finite-mode approximations. The proof applies the companion viscous energy decay result, rewrites it via the discrete energy definition, and extracts the norm bound from the squared-norm comparison.
Claim. Let $N$ be a natural number, let $ν ≥ 0$, let $B$ be a bilinear convection operator on the space of Fourier coefficients with modes up to $N$ in three dimensions such that $⟨B(u,u),u⟩=0$ for all $u$, and let $u:ℝ→$ (Euclidean space over modes × 3) be differentiable with derivative equal to $ν$ times the Laplacian coefficient minus $B(u,u)$. Then $‖u(t)‖ ≤ $‖u(0)‖ for every $t≥0$.
background
The module extends the 2D Galerkin construction to three dimensions on the torus T³ with Fourier modes truncated to [-N,N]³. GalerkinState3 is the Euclidean space of real coefficients indexed by those modes times the three velocity components. ConvectionOp3 is the type of bilinear maps that realize the projected nonlinearity, while EnergySkewHypothesis3 encodes the structural identity ⟨B(u,u),u⟩=0 that makes the nonlinearity energy-conserving. The right-hand side galerkinNSRHS3 combines viscous Laplacian action with the convection term. The upstream viscous_energy_bound3 theorem already establishes the corresponding decay for the discrete energy functional (1/2)‖u‖².
proof idea
The tactic proof first calls viscous_energy_bound3 to obtain the energy inequality at time t. It then rewrites that inequality using the definition of discreteEnergy3 to reach (1/2)‖u t‖² ≤ (1/2)‖u 0‖². Linarith closes the comparison of squared norms, after which le_of_sq_le_sq together with nonnegativity of the norm yields the desired bound on ‖u t‖.
why it matters
The result supplies the basic L2 control for any Galerkin trajectory, a prerequisite for subsequent enstrophy estimates and for passing to the limit as N grows. It directly implements the energy identity listed in the module header and appears in the paper RS_NavierStokes_BKM.tex §4 as part of the Galerkin approximation argument. Within the Recognition Science framework it supports the discrete sub-Kolmogorov setting by guaranteeing that truncated velocity fields remain bounded independently of the truncation level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.