inviscid_energy_deriv_zero3
plain-language theorem explainer
The result shows that discrete kinetic energy is conserved along trajectories of the inviscid 3D Galerkin system when the velocity satisfies the projected Euler equation. Spectral fluid dynamicists working on truncated Navier-Stokes models cite it to confirm the energy identity before adding viscosity. The proof differentiates the squared Euclidean norm, scales to the energy functional, and cancels the inner-product term via the skew-symmetry hypothesis.
Claim. Let $B$ be a bilinear convection operator on the $N$-mode Galerkin space that satisfies the energy-skew condition $⟨B(u,u),u⟩=0$ for every state $u$. Suppose a curve $u(t)$ obeys $u'(t)=-B(u(t),u(t))$ at time $t$. Then the discrete energy $E(s)=½‖u(s)‖² has derivative zero at $t$.
background
The module develops a Fourier-Galerkin truncation of the 3D incompressible Navier-Stokes equations on the torus T³ using modes in [-N,N]³. GalerkinState3 is the Euclidean space of real coefficients indexed by these modes times the three velocity components. ConvectionOp3 encodes the projected nonlinear term (u·∇)u. discreteEnergy3 is defined as half the squared Euclidean norm of the coefficient vector, which equals the L² kinetic energy of the truncated field. EnergySkewHypothesis3 is the structural assumption that the inner product of B(u,u) with u vanishes identically; the module doc states this is the key energy identity for the Galerkin nonlinearity.
proof idea
The tactic proof first applies HasDerivAt.norm_sq to obtain the derivative of the squared norm, yielding twice the inner product of u(t) with the given velocity derivative. Scaling by 1/2 produces the derivative of discreteEnergy3. A short calc then rewrites the inner product as minus the inner product of B(u,u) with u, invokes real_inner_comm to swap arguments, and applies the skew hypothesis to conclude the term is zero. Substitution back into the energy derivative finishes the argument.
why it matters
This theorem supplies the inviscid energy conservation step inside the 3D Galerkin framework of RS_NavierStokes_BKM.tex §4. It is the direct 3D counterpart of the 2D energy identity and is required before the viscous dissipation estimate and enstrophy bounds can be stated. The result sits at the base of the discrete sub-Kolmogorov analysis; without it the subsequent control of spectral enstrophy by νN² would lack its conservative reference case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.