functionalsNormSq
plain-language theorem explainer
This definition supplies a concrete instance of the four CPM functionals on the N-dimensional state space, with defect mass, orthogonal mass, energy gap, and tests each equal to the squared norm of the input state. Researchers building the classical bridge from Recognition Science to 2D fluid models would cite it to obtain a minimal, assumption-free hypothesis bundle for the Galerkin discretization. The definition is a direct record construction that assigns the same lambda expression to every field.
Claim. For each natural number $N$, the CPM functionals on the state space are the structure in which defect mass, orthogonal mass, energy gap, and the test functional are each the map sending a state $u$ to the squared Euclidean norm of $u$.
background
The CPM2D module instantiates the core CPM model from LawOfExistence for the finite-dimensional 2D Galerkin model. The Functionals structure requires four maps from State N to the reals: defectMass, orthoMass, energyGap, and tests. constantsOne provides a constants bundle with every entry equal to 1. Upstream definitions in ILG.CPMInstance interpret analogous functionals via kernel-weighted squared deviations for defect mass and excess energy integrals for the energy gap.
proof idea
The definition is a direct record construction of type Functionals N that sets each of the four fields to the lambda expression returning the squared norm of its argument.
why it matters
It is consumed by hypothesisNormSq to produce a no-assumption CPM hypothesis instance. This supports Milestone M4 in CPM2D by furnishing the functionals for the classical bridge to fluid models. The module packages analytic requirements explicitly in Hypothesis structures rather than proving them, leaving closure of the fluid inequalities as an open question for downstream work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.