viscous_energy_bound_from_initial
plain-language theorem explainer
viscous_energy_bound_from_initial shows that discrete kinetic energy along solutions of the viscous Galerkin Navier-Stokes system is nonincreasing for nonnegative viscosity. Researchers deriving a priori bounds on finite-mode fluid models would cite this result. The proof is a one-line wrapper that applies the antitone property of the energy map established by the companion viscous_energy_antitone theorem.
Claim. Let $N$ be a natural number, let $ν ≥ 0$, let $B$ be a convection operator on the $N$-mode Galerkin space satisfying the energy skew-symmetry hypothesis $⟨B(u,u),u⟩=0$, and let $u:ℝ→$Galerkin state be differentiable with $u'(t)=νΔu(t)-B(u(t),u(t))$. Then for all $t≥0$ the discrete kinetic energy satisfies $E(u(t))≤E(u(0))$.
background
The module constructs a finite-dimensional Fourier-mode truncation of 2D incompressible Navier-Stokes on the torus. GalerkinState is the Euclidean space of velocity coefficients indexed by the truncated modes and two components. ConvectionOp is an abstract bilinear map whose only enforced property is the skew-symmetry encoded in EnergySkewHypothesis. The right-hand side galerkinNSRHS is defined as ν times the Laplacian coefficients minus B(u,u). Discrete energy is the standard quadratic form (1/2)‖u‖².
proof idea
The argument calls viscous_energy_antitone on the supplied parameters to obtain that t↦discreteEnergy(u t) is antitone. It then specializes the antitone relation at the points 0 and t (using t≥0) and simplifies. The entire proof is a one-line wrapper around the antitone lemma.
why it matters
The result supplies the energy monotonicity required by the downstream theorem viscous_norm_bound_from_initial. It belongs to milestone M1 of the ClassicalBridge, which builds a concrete finite-dimensional model whose algebraic energy identity can be compared with the continuous theory. The argument rests on the energy-skew hypothesis that encodes the projected nonlinearity, a prerequisite for later inviscid-limit or higher-dimensional work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.