inviscid_energy_deriv_zero
plain-language theorem explainer
Inviscid energy conservation holds pointwise for the truncated 2D Galerkin system whenever the convection operator obeys the skew-symmetry condition. Researchers working on finite-mode approximations to incompressible flow would invoke this result to verify that the discrete kinetic energy remains constant along trajectories. The argument applies the chain rule to the squared Euclidean norm, halves the result, and cancels the inner product via the given skew hypothesis.
Claim. Let $B$ be a convection operator on the $N$-mode Galerkin state space satisfying $⟨B(v,v), v⟩ = 0$ for all velocity fields $v$. If a trajectory $u(t)$ obeys the ODE $u'(t) = -B(u(t), u(t))$ at time $t$, then the derivative of the discrete energy $E(u) = ½ ‖u‖² vanishes: d/dt E(u(t)) = 0.
background
The Galerkin2D module constructs a finite-dimensional model for 2D incompressible Navier-Stokes on the torus by truncating to the first N Fourier modes. GalerkinState N is the Euclidean space of velocity coefficients indexed by modes times two components. The convection operator B abstracts the projected nonlinearity, to be replaced later by explicit Fourier convolution. discreteEnergy is defined as half the squared norm of the state vector. EnergySkewHypothesis encodes the single algebraic property required for conservation: the inner product of B(u,u) with u itself is zero. This setup isolates the inviscid energy identity before introducing viscosity or taking continuum limits. Upstream results include the definition of discreteEnergy and the structure of EnergySkewHypothesis, which directly supplies the skew property used in the cancellation.
proof idea
The proof first invokes HasDerivAt.norm_sq on the given derivative of u to obtain the derivative of the squared norm. It then scales by one-half using const_mul to reach the derivative of discreteEnergy. A short calculation applies the skew property from HB to show that the inner product term vanishes, after which simplification yields the zero derivative.
why it matters
This result supplies the algebraic energy conservation identity for the inviscid case in the M1 milestone of the Galerkin2D development. It serves as the discrete precursor to the energy estimates needed for uniform bounds in the viscous system. Within the Recognition framework it anchors the classical bridge by confirming that the truncated model inherits the conservation law of the underlying Euler equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.