functionalsNormSq
functionalsNormSq supplies a concrete realization of the four CPM functionals for the N-dimensional Galerkin state, with each functional returning the squared norm of the input vector. Researchers modeling 2D incompressible flow via finite-dimensional projections in the CPM framework would cite this when building a LawOfExistence model instance. The definition is a direct record construction assigning the squared-norm expression to defectMass, orthoMass, energyGap, and tests.
claimLet $N$ be a natural number. The functionals are given by defectMass$(u) = ||u||^2$, orthoMass$(u) = ||u||^2$, energyGap$(u) = ||u||^2$, tests$(u) = ||u||^2$ for states $u$ in the $N$-dimensional space.
background
The Functionals structure collects the four maps defectMass, orthoMass, energyGap, and tests from State N to real numbers, as required by the CPM LawOfExistence Model. The CPM2D module instantiates the CPM core for the finite-dimensional 2D Galerkin model from Galerkin2D, packaging functionals explicitly so that downstream theorems can declare their assumptions without axioms. Upstream results include constantsOne, which sets all constants to one, and the ILG CPMInstance definitions that provide analogous defect mass and energy gap concepts in the continuous setting.
proof idea
The definition directly constructs the Functionals record by setting each of the four fields to the function that computes the squared Euclidean norm of its argument.
why it matters in Recognition Science
This supplies the concrete functionals for hypothesisNormSq, which builds a no-assumption CPM hypothesis instance. It serves as the minimal model in the ClassicalBridge for the Galerkin2D approximation, enabling precise dependency statements in fluid proofs. It supports the bridge to classical models without invoking the full Recognition forcing chain or phi-ladder at this stage.
scope and limits
- Does not prove any analytic inequalities or estimates for the fluid system.
- Does not relate the functionals to the phi-ladder or Recognition constants.
- Does not establish existence or uniqueness results for the underlying equations.
formal statement (Lean)
89noncomputable def functionalsNormSq (N : ℕ) : Functionals N :=
proof body
Definition body.
90 { defectMass := fun u => ‖u‖ ^ 2
91 orthoMass := fun u => ‖u‖ ^ 2
92 energyGap := fun u => ‖u‖ ^ 2
93 tests := fun u => ‖u‖ ^ 2 }
94
95/-- A no-assumption CPM hypothesis instance using `constantsOne` and `functionalsNormSq`. -/