constantsOne
plain-language theorem explainer
This definition supplies an all-ones instance of the CPM constants bundle for the 2D fluid model. Workers on the ClassicalBridge.Fluids.CPM2D module cite it to instantiate the core law of existence with unit values. The construction assigns each parameter to one and verifies non-negativity by direct computation.
Claim. Define the constant bundle $C$ by setting $K_{rm net}=1$, $C_{rm proj}=1$, $C_{rm eng}=1$, $C_{rm disp}=1$, each with the non-negativity condition $0leq cdot$.
background
The Constants structure from the LawOfExistence module is an abstract bundle of four real parameters Knet, Cproj, Ceng, Cdisp, each accompanied by a non-negativity proof. The CPM2D module instantiates the CPM core for the finite-dimensional 2D Galerkin model of fluids. The module documentation notes that nontrivial analytic inequalities are packaged in a separate Hypothesis structure to avoid axioms or sorry in downstream results. The upstream Constants documentation describes it as the abstract bundle of CPM constants.
proof idea
The definition builds the record explicitly by assigning the value 1 to each of the four fields and applies norm_num to each non-negativity obligation.
why it matters
This supplies the constant values required by the functionalsNormSq and hypothesisNormSq definitions in the same module. It fills the concrete instance needed for the CPM2D milestone M4, which packages hypotheses for the 2D fluid model without proving the analytic inequalities. It connects to the LawOfExistence core by providing a trivial but explicit Constants bundle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.