Functionals
plain-language theorem explainer
The declaration defines a record type holding four real-valued maps on the discrete 2D Galerkin state space at truncation level N. Researchers building CPM instances for finite Galerkin fluid models cite this structure when supplying the data fields for LawOfExistence.Model. It is introduced as a plain structure definition with no further content or computation.
Claim. A structure consisting of four maps from the space of Galerkin states at truncation level $N$ to the reals: defect mass, orthogonal mass, energy gap, and test functional.
background
The module CPM2D instantiates the CPM core for the finite-dimensional 2D Galerkin model from Galerkin2D. State N is the abbreviation for GalerkinState N, the Euclidean space of velocity coefficients over truncated modes and two components. The four maps are exactly the fields required by the Model structure in LawOfExistence, which takes a type parameter beta and records defectMass, orthoMass, energyGap, and tests as beta to real maps.
proof idea
This is a structure definition; it introduces the type and its four projection fields with no lemmas or tactics applied.
why it matters
The structure supplies the functional data that Hypothesis bundles with Constants and the three coercivity inequalities to produce a concrete CPM.LawOfExistence.Model instance. It supports the M4 milestone by allowing downstream theorems to state their analytic dependencies explicitly. functionalsNormSq later supplies the concrete squared-norm realization, and ILG.CPMInstance uses the same pattern for gravitational configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.