viscous_energy_deriv_le_zero
plain-language theorem explainer
The theorem establishes that for a solution u(t) of the viscous Galerkin Navier-Stokes system with energy-skew nonlinearity, the time derivative of the discrete kinetic energy equals ν times the inner product of velocity with its Laplacian projection. Researchers working on discrete fluid models or energy estimates in truncated Fourier systems would cite this result. The proof differentiates the squared norm, scales to the energy functional, cancels the convective term via skew-symmetry, and isolates the viscous contribution.
Claim. Let $E(u) = (1/2) ||u||^2$ denote the discrete kinetic energy. Suppose $u : ℝ →$ GalerkinState $N$ satisfies $du/dt(t) = ν Δu(t) - B(u(t), u(t))$, where the convection operator $B$ obeys $⟨B(v,v), v⟩ = 0$ for all $v$. Then $dE(u(t))/dt = ν ⟨u(t), Δu(t)⟩$.
background
In the Galerkin2D module a finite-dimensional Fourier-mode truncation of 2D incompressible Navier-Stokes on the torus is introduced. The state space is the Euclidean space GalerkinState N over the product of truncated modes and two velocity components. The convection operator ConvectionOp N is an abstract bilinear map for the projected nonlinearity, later to be realized by explicit Fourier convolution plus Leray projection. The right-hand side of the dynamics is given by galerkinNSRHS ν B u = ν • laplacianCoeff u - B u u, where laplacianCoeff multiplies each mode coefficient by -|k|². Discrete energy is defined by discreteEnergy u = (1/2) ||u||². The EnergySkewHypothesis B encodes the single algebraic requirement ⟨B u u, u⟩ = 0 that guarantees inviscid energy conservation.
proof idea
Apply HasDerivAt.norm_sq to the curve u to obtain the derivative of ||u s||² as 2 ⟨u t, galerkinNSRHS ν B (u t)⟩. Scale the result by 1/2 to recover the derivative of discreteEnergy. Expand the inner product with galerkinNSRHS using its definition and the skew property from EnergySkewHypothesis, which forces the convective term to vanish after invoking real_inner_comm. The surviving term is exactly ν ⟨u t, laplacianCoeff (u t)⟩. Rewrite the scaled derivative to match this expression.
why it matters
The identity supplies the explicit energy derivative required to prove monotonicity under positive viscosity. It is invoked directly by viscous_energy_deriv_nonpos to obtain the non-positive derivative and by viscous_energy_antitone to conclude that discrete energy is antitone along solutions. Within the Recognition Science framework the result advances the ClassicalBridge by furnishing a discrete model whose dissipation structure mirrors continuum Navier-Stokes, linking the foundational forcing chain to classical fluid dynamics. The construction prepares the ground for continuum limits in subsequent milestones.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.