cmin_pos
plain-language theorem explainer
If the three CPM constants are strictly positive then the derived coercivity constant is positive. Abstract model builders cite this to guarantee that the energy gap controls defect mass in the Coercive Projection Method. The proof first shows the product of the three constants is positive via iterated multiplication, then obtains positivity of the reciprocal and unfolds the definition of cmin.
Claim. Let $C$ be a CPM constants bundle with $0 < K_{net}$, $0 < C_{proj}$ and $0 < C_{eng}$. Then $0 < c_{min}(C)$, where $c_{min}(C) := (K_{net} · C_{proj} · C_{eng})^{-1}$.
background
The Law of Existence module supplies a domain-agnostic formalization of the Coercive Projection Method in three parts: projection-defect inequality, coercivity factorization, and aggregation. It works with an abstract state type together with four aggregate functionals: defectMass, orthoMass, energyGap and tests. The Constants structure bundles four nonnegative reals Knet, Cproj, Ceng and Cdisp, each carrying its own nonnegativity hypothesis.
proof idea
The tactic proof first applies mul_pos twice to the three input inequalities to obtain positivity of the triple product. It then invokes inv_pos.mpr on that product. The final simpa tactic unfolds the definition of cmin to conclude the result.
why it matters
This lemma is invoked by the toy model certificate in URCGenerators.CPMMethodCert to verify that a concrete instance satisfies the basic coercivity requirement. It closes the foundational positivity check inside the abstract CPM logic before defect-energy inequalities are applied, ensuring the coercivity constant remains well-defined whenever the input constants are positive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.