viscous_energy_deriv3
plain-language theorem explainer
The viscous energy derivative theorem states that along any differentiable trajectory satisfying the 3D Galerkin Navier-Stokes system with viscosity ν ≥ 0 and energy-skew convection operator B, the time derivative of the discrete energy equals ν times the inner product of the state with its spectral Laplacian coefficient. Researchers in spectral Galerkin methods or discrete energy estimates for incompressible flow would cite this identity. The proof differentiates the squared norm, scales by one-half, cancels the nonlinear term via skew-symmety
Claim. Let $u : ℝ → ℝ^M$ be a curve in the finite-dimensional space of Fourier coefficients for modes up to wavenumber $N$ in three dimensions, satisfying $u'(t) = ν Δu(t) - B(u(t),u(t))$ where $B$ obeys ⟨B(v,v),v⟩ = 0. Then $d/dt (½ ‖u(t)‖²) = ν ⟨u(t), Δu(t)⟩$.
background
In the 3D spectral Galerkin truncation the state space consists of Euclidean vectors indexed by Fourier modes in [-N,N]³ with three velocity components. The convection operator is the bilinear map representing the projected nonlinearity. The energy-skew hypothesis asserts that this operator satisfies ⟨B u u, u⟩ = 0 for every state u. The discrete energy is defined as ½ ‖u‖². The right-hand side of the Galerkin system is ν times the spectral Laplacian coefficient minus the convection term, where the Laplacian coefficient multiplies each mode by -|k|².
proof idea
Differentiate the squared norm via HasDerivAt.norm_sq to obtain the inner product against the full right-hand side. Scale by one-half to recover the derivative of the discrete energy. Apply the skew-symmetry hypothesis to show the convection inner product vanishes. Simplify the remaining inner product against the right-hand side to isolate ν times the Laplacian inner product, then substitute back.
why it matters
This identity supplies the exact dissipation rate that feeds the antitone theorem viscous_energy_antitone3, which concludes that discrete energy is nonincreasing. It supplies the viscous dissipation step in the Galerkin approximation for 3D Navier-Stokes as described in the module documentation and the paper reference RS_NavierStokes_BKM.tex §4. Within the Recognition Science framework it supports control of energy decay in the truncated system that connects to the discrete sub-Kolmogorov estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.