Functionals
Four real-valued maps on the truncated 2D Galerkin velocity space are packaged to supply the defect, orthogonality, energy-gap and test data required by the CPM existence model. Analysts working with finite-mode approximations to incompressible flow would cite this packaging when instantiating the LawOfExistence framework. The declaration is a direct structure definition carrying no proof content.
claimLet $S_N$ be the space of Galerkin states at truncation level $N$. A functionals bundle consists of four maps $d,o,e,t:S_N→ℝ$ that furnish defect mass, orthogonal mass, energy gap and test values for the CPM model.
background
The CPM2D module instantiates the core CPM existence machinery for a finite-dimensional 2D Galerkin truncation of the velocity field. The state type is the Euclidean space over the product of truncated modes and the two velocity components. Upstream, the LawOfExistence.Model structure is parameterized by an arbitrary type β and requires exactly these four functional fields together with a constants bundle.
proof idea
The declaration is a structure definition that simply declares the four maps; no lemmas are applied and no tactics are used.
why it matters in Recognition Science
This structure supplies the data component inside the Hypothesis bundle that constructs a Model for the LawOfExistence theorem. It is instantiated concretely by the functionalsNormSq definition that sets each map to the squared Euclidean norm. The construction therefore supplies the missing piece that lets the 2D Galerkin system satisfy the abstract CPM hypotheses without introducing new axioms.
scope and limits
- Does not prove the projection-defect, energy-control or dispersion inequalities.
- Does not specify how the maps are computed from the velocity coefficients.
- Does not extend to the infinite-dimensional function space.
- Does not constrain the constants that accompany the functionals.
formal statement (Lean)
29structure Functionals (N : ℕ) where
30 defectMass : State N → ℝ
31 orthoMass : State N → ℝ
32 energyGap : State N → ℝ
33 tests : State N → ℝ
34
35/-- Hypothesis bundle: a CPM instance for `GalerkinState N`.
36
37This is *exactly* the data needed to build a `CPM.LawOfExistence.Model`.
38-/