discreteEnergy
plain-language theorem explainer
discreteEnergy supplies the discrete kinetic energy for a Galerkin state u as half its squared Euclidean norm on the coefficient space. Researchers deriving energy conservation or dissipation in truncated 2D Navier-Stokes models within Recognition Science cite this definition when establishing algebraic identities for the inviscid and viscous cases. The definition is a direct one-line expression using the built-in norm on EuclideanSpace.
Claim. Let $N$ be a natural number and let $u$ be a Galerkin state consisting of real velocity coefficients indexed by the truncated modes and two components. The discrete energy is $E(u) := (1/2) ||u||^2$, where $||·||$ is the Euclidean norm on the coefficient space.
background
The Galerkin2D module builds a finite-dimensional Fourier-truncated model for 2D incompressible Navier-Stokes on the torus, with the explicit goal of obtaining a concrete discrete state space and the basic algebraic energy identity for the inviscid case. GalerkinState N is the EuclideanSpace ℝ over the product of the mode set and Fin 2, so that inner products and norms are immediately available for energy calculations. The module isolates the single algebraic property of the convection operator needed for energy conservation, namely that the inner product of B(u,u) with u vanishes.
proof idea
This is a one-line wrapper that directly applies the squared-norm expression on the EuclideanSpace type for the Galerkin coefficients. No lemmas beyond the standard norm definition are invoked.
why it matters
This definition supplies the energy functional used in every energy estimate in the module. It appears directly in inviscid_energy_deriv_zero to obtain conservation under the EnergySkewHypothesis, and in viscous_energy_antitone together with viscous_energy_bound_from_initial to obtain monotonicity and initial-data bounds for positive viscosity. The construction completes the basic energy identity step of Milestone M1 and supplies the discrete counterpart to continuum kinetic energy, consistent with the Recognition Science forcing chain that derives classical physics from the J-uniqueness and eight-tick structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.