Functionals
plain-language theorem explainer
The Functionals structure collects four maps from the discrete 2D Galerkin state space to the reals that supply the exact data fields required by the CPM LawOfExistence.Model. Researchers instantiating finite-dimensional fluid models cite it when packaging a CPM instance for Galerkin truncation. It is a direct structure definition with no proof obligations.
Claim. For each truncation level $N$, the functionals are four maps from the Galerkin state space to the reals: defect mass, orthogonal mass, energy gap, and tests.
background
State N is the abbrev for GalerkinState N, the Euclidean space of velocity coefficients over the truncated modes times two components. The LawOfExistence.Model structure is defined with fields C : Constants together with exactly these four maps defectMass, orthoMass, energyGap, tests : β → ℝ. The module CPM2D packages the CPM core for the finite-dimensional 2D Galerkin model while keeping analytic inequalities explicit in a separate Hypothesis structure rather than using axioms.
proof idea
This is a structure definition that directly declares the four required maps; no lemmas or tactics are applied.
why it matters
It supplies the functional data consumed by the sibling Hypothesis structure, which in turn supplies the exact data needed to build a CPM.LawOfExistence.Model for GalerkinState N. This step forms part of the classical bridge that lets downstream theorems state their dependence on coercivity bounds without axioms. The construction remains agnostic to the concrete forms of the maps and to any connection with the phi-ladder or forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.