model
plain-language theorem explainer
This definition assembles a CPM Model for the truncated 2D Galerkin state from a supplied Hypothesis bundle that encodes the required functionals and control inequalities. Fluid dynamicists using spectral methods to approximate Navier-Stokes flows would reference it when embedding the Recognition cost structure into a discrete model. The construction is a direct record literal that transfers the defectMass, orthoMass, energyGap, tests, and the three control inequalities straight from the hypothesis fields.
Claim. Let $H$ be a hypothesis bundle for truncation level $N$, containing constants $C$, functionals $F$, and the three control inequalities (projection-defect bound on defect mass, energy-control bound on orthogonal mass, and dispersion bound). The CPM model for the Galerkin state at level $N$ is the instance whose cost functional is $C$, defect mass is $F$'s defect mass, orthogonal mass is $F$'s orthogonal mass, energy gap is $F$'s energy gap, tests are $F$'s tests, and whose three control inequalities are exactly the projection-defect, energy-control, and dispersion statements supplied in $H$.
background
The CPM2D module instantiates the CPM core from LawOfExistence for the finite-dimensional 2D Galerkin model. State is the abbrev for GalerkinState at truncation level $N$. The Hypothesis structure packages constants $C$, the four functionals (defectMass, orthoMass, energyGap, tests), and the three explicit inequalities: projection_defect requires defectMass $a$ ≤ $K_{net} · C_{proj} ·$ orthoMass $a$; energy_control requires orthoMass $a$ ≤ $C_{eng} ·$ energyGap $a$; dispersion requires orthoMass $a$ ≤ $C_{disp} ·$ tests $a$ for every state $a$. Upstream, CostAlgebra.H reparametrizes the base cost to $H(x) = J(x) + 1$, converting the Recognition Composition Law into the standard d'Alembert form $H(xy) + H(x/y) = 2 H(x) H(y)$.
proof idea
The definition is a direct record construction that populates every field of the Model structure by selecting the matching component from the input Hypothesis: C from H.C, defectMass from H.F.defectMass, orthoMass from H.F.orthoMass, energyGap from H.F.energyGap, tests from H.F.tests, and the three inequalities from the corresponding Hypothesis fields projection_defect, energy_control, and dispersion.
why it matters
This definition supplies the concrete Model instance required by the CPMBridge structure and thereby feeds the RSNSBridgeSpec and DiscreteModel used in classical fluids approximations. It realizes milestone M4 by packaging the Galerkin-specific controls for the Recognition Science cost model, allowing traceability from the discrete state to the underlying J-cost functional without proving the inequalities here. It connects to the broader framework by instantiating the Model type from LawOfExistence for use in bridge constructions to Navier-Stokes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.