model
plain-language theorem explainer
The definition assembles a CPM Model on the Galerkin state space at truncation N by extracting constants, four functionals, and three control inequalities directly from a supplied Hypothesis bundle. Discrete fluid modelers and RS-NS bridge constructions cite it when instantiating the core existence law for 2D spectral approximations without introducing axioms. The construction is a direct record field copy with no lemmas or computation.
Claim. Given a Hypothesis bundle $H$ for truncation level $N$, the model is the CPM Model on GalerkinState $N$ whose constants are $H.C$, whose defectMass, orthoMass, energyGap and tests functionals are taken from $H.F$, and whose projection-defect, energy-control and dispersion inequalities are the three properties supplied by $H$.
background
Module CPM2D instantiates the CPM core (from LawOfExistence) for the finite-dimensional 2D Galerkin model. The Hypothesis structure is the exact data bundle required: it contains Constants $C$, the four functionals (defectMass, orthoMass, energyGap, tests), and the three inequalities that stand in for the analytic estimates (projection_defect: defectMass $a$ ≤ $K_{net} C_{proj}$ orthoMass $a$; energy_control: orthoMass $a$ ≤ $C_{eng}$ energyGap $a$; dispersion: orthoMass $a$ ≤ $C_{disp}$ tests $a$). State is the type alias for GalerkinState $N$. Upstream, Model is the record type defined in CPM.LawOfExistence; the shifted cost $H(x)=J(x)+1$ from CostAlgebra supplies the recognition-functional background used throughout the framework.
proof idea
This is a definition whose body is a direct record constructor. It copies the eight fields (C, defectMass, orthoMass, energyGap, tests, projection_defect, energy_control, dispersion) from the input Hypothesis $H$ into the Model record. No lemmas are invoked; the construction is a one-line wrapper that performs only field projection.
why it matters
The definition supplies the concrete Model instance required by CPMBridge and by the RSNSBridgeSpec used in the fluids bridge. It realizes the M4 milestone of packaging the 2D Galerkin discretization into the Recognition Science framework, allowing downstream discrete models (DiscreteModel, DiscretizationKind) to depend on explicit hypotheses rather than axioms. It sits between the core CPM.LawOfExistence.Model and the bridge-local CPMBridge structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.