constantsOne
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.