viscous_energy_nonpos3
plain-language theorem explainer
The theorem establishes nonpositivity of the viscous term ν ⟨u(t), laplacianCoeff3(u(t))⟩ for nonnegative viscosity in the 3D spectral Galerkin truncation of Navier-Stokes. Researchers deriving a priori energy bounds for truncated fluid equations cite it when proving monotonicity of the discrete energy. The proof is a one-line wrapper applying the multiplication rule for nonnegative and nonpositive reals to the viscosity hypothesis and the self-inner-product negativity of the spectral Laplacian.
Claim. Let ν ≥ 0. For a differentiable curve u(t) in the finite-dimensional Galerkin state space on T³ with N modes per direction, satisfying the truncated Navier-Stokes equation whose convection operator obeys the energy-skew condition ⟨B(u,u),u⟩=0, the viscous contribution satisfies ν ⟨u(t), Δu(t)⟩ ≤ 0, where Δ denotes the Fourier multiplier by −|k|² on each retained mode.
background
GalerkinState3 N is the Euclidean space of velocity fields whose Fourier coefficients are supported on modes with |k_i| ≤ N in each coordinate and three velocity components. ConvectionOp3 N is the type of bilinear maps representing the projected nonlinearity, while EnergySkewHypothesis3 asserts that the inner product of B(u,u) with u vanishes identically, which encodes the skew-symmetry preventing the nonlinearity from altering L² energy. The operator laplacianCoeff3 multiplies each mode coefficient by −kSq3(k), so its self-inner-product expands to a sum of −k² |û_k|² terms and is therefore non-positive.
proof idea
This is a one-line wrapper that applies mul_nonpos_of_nonneg_of_nonpos to the hypothesis 0 ≤ ν together with the lemma laplacianCoeff3_inner_self_nonpos evaluated at u t.
why it matters
The result is invoked by viscous_energy_antitone3 to conclude that discreteEnergy3 is antitone along solutions. It supplies the viscous dissipation step in the Galerkin approximation analysis of RS_NavierStokes_BKM.tex §4 and supports the connection to the discrete sub-Kolmogorov framework. In the Recognition Science setting it contributes the energy-decay control required for the spectral truncation before any continuum limit is taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.