constantsOne
constantsOne supplies the all-ones instance of the CPM Constants structure for the 2D Galerkin fluid model. Workers on the classical bridge cite it when they want a parameter-free base case for norm-squared functionals. The definition directly populates the four fields with 1 and discharges the four nonnegativity conditions by norm_num.
claimLet Constants be the structure whose fields are nonnegative reals $K_{net}$, $C_{proj}$, $C_{eng}$, $C_{disp}$. The bundle constantsOne is the instance in which each field equals 1.
background
The CPM2D module instantiates the core CPM structure from LawOfExistence for the finite-dimensional 2D Galerkin model. Constants is the abstract bundle containing the four real parameters Knet, Cproj, Ceng, Cdisp together with proofs that each is nonnegative. The module packages any required analytic inequalities inside an explicit Hypothesis record so that downstream statements can list their exact dependencies without axioms or sorry.
proof idea
The definition constructs the Constants record by assigning the literal value 1 to each of the four fields. Each nonnegativity obligation is discharged by the norm_num tactic.
why it matters in Recognition Science
constantsOne supplies the concrete parameter set used by functionalsNormSq and hypothesisNormSq to build the norm-squared instance of Hypothesis. It therefore anchors the M4 milestone in the classical fluids bridge by giving an explicit, assumption-free starting point for the all-ones case.
scope and limits
- Does not assign any physically measured values to the constants.
- Does not prove any analytic inequalities for the fluid equations.
- Does not extend beyond the 2D Galerkin discretization.
formal statement (Lean)
78noncomputable def constantsOne : Constants :=
proof body
Definition body.
79 { Knet := 1
80 Cproj := 1
81 Ceng := 1
82 Cdisp := 1
83 Knet_nonneg := by norm_num
84 Cproj_nonneg := by norm_num
85 Ceng_nonneg := by norm_num
86 Cdisp_nonneg := by norm_num }
87
88/-- Concrete functionals: everything is measured by `‖u‖^2` (a nonnegative scalar). -/