EnergyFunctional
plain-language theorem explainer
This structure declares an optional real-valued energy map on the state space of any discrete dynamical model intended to approximate Navier-Stokes. Numerical analysts establishing a priori bounds or stability for discrete fluid schemes would cite it when extending the minimal interface. The definition is a direct structure declaration with a single field of type State to reals.
Claim. For a discrete model $D$, an energy functional is a map $E : D.State → ℝ$.
background
The module supplies a minimal interface for discrete Navier-Stokes approximations without fixing a discretization (Galerkin versus grid). A DiscreteModel is a structure containing a State type (e.g., truncated Fourier coefficients), a DiscretizationKind tag, and a step function that advances the state from NSParams and TimeStep. The local setting deliberately leaves concrete models to downstream files so that the interface can later relate to LNAL spatial semantics and CPM defect/energy functionals. Upstream dependencies include the 2D Galerkin State abbrev from CPM2D and the general DiscreteModel definition itself.
proof idea
One-line structure definition that directly introduces the field E as a function from the model's State type to the reals. No lemmas or tactics are invoked.
why it matters
The declaration supplies the energy map slot required for future a priori bounds in discrete fluid models that sit between the Recognition framework's spectral emergence (E) and discrete vorticity structures. It fills the interface gap noted in the module doc for connecting to CPM.LawOfExistence.Model, though no parent theorems yet consume it. The choice of discretization remains open, as the module explicitly defers Galerkin-on-torus or grid instantiations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.