viscous_energy_deriv_nonpos
plain-language theorem explainer
In the finite-mode Galerkin truncation of 2D Navier-Stokes, if a differentiable curve u satisfies the discrete equation with viscosity ν ≥ 0 and the convection operator obeys the energy-skew condition, then the time derivative of discrete kinetic energy equals ν times the inner product of u(t) with its Laplacian coefficient, and this quantity is non-positive. Researchers deriving energy estimates for spectral fluid models would cite it. The proof is a term-mode refinement that pairs the derivative identity lemma with the non-positivity of the L
Claim. Let $N$ be a natural number, let $ν ≥ 0$, let $B$ be a bilinear convection operator on the space of Galerkin states satisfying $⟨B(v,v),v⟩=0$ for every state $v$, and let $u:ℝ→$ Galerkin states be differentiable at $t$ with derivative equal to $ν$ times the Laplacian coefficient of $u(t)$ minus $B(u(t),u(t))$. Then the derivative at $t$ of the discrete kinetic energy $½‖u(s)‖² equals $ν⟨u(t),$ Laplacian coefficient of $u(t)⟩$, and this product is ≤ 0.
background
The Galerkin2D module builds a finite-dimensional Fourier-mode truncation of 2D incompressible Navier-Stokes on the torus, with states represented as Euclidean vectors of velocity coefficients over truncated modes and two components. Discrete kinetic energy is defined as half the squared norm of the state. The convection operator is kept abstract but must satisfy the algebraic skew-symmetry $⟨B(u,u),u⟩=0$, which guarantees energy conservation when viscosity vanishes. The right-hand side of the dynamics is $ν$ times the Laplacian coefficient (multiplication by $-|k|²$ on each mode) minus the convection term.
proof idea
The proof is a term-mode refinement. It supplies the first conjunct directly from the lemma that computes the derivative of discrete energy along solutions of the discrete Navier-Stokes equation. The second conjunct follows by invoking the lemma that the inner product of any state with its own Laplacian coefficient is non-positive, then applying the arithmetic fact that a non-negative scalar times a non-positive scalar is non-positive.
why it matters
This theorem supplies the viscous dissipation identity for the discrete system, confirming that the Laplacian term produces non-positive energy change once the energy-skew hypothesis on the nonlinearity is in place. It completes the basic energy balance for the viscous case in the Galerkin truncation and sits upstream of any later long-time decay or stability arguments in the ClassicalBridge. No downstream uses are recorded yet, leaving open its role in global existence or continuum-limit comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.