toyModel_cmin_pos
plain-language theorem explainer
The lemma shows that the coercivity constant cmin is strictly positive on the toy CPM model. Workers on the standalone CPM certificate cite it to witness consistency of the positivity assumptions in the verified predicate. The proof extracts the three constant inequalities by simplification on the toy model definition, then applies the general cmin_pos result from LawOfExistence.
Claim. For the toy model whose constants satisfy $0 < K_{net}$, $0 < C_{proj}$, and $0 < C_{eng}$, the coercivity constant obeys $0 < c_{min}$ where $c_{min} = 1/(K_{net} C_{proj} C_{eng})$.
background
The module supplies a standalone CPM method certificate that certifies generic A/B/C consequences for any Model and consistency via a concrete toy witness. The toyModel is the instance in which all functionals are constantly 1. The definition cmin from LawOfExistence is the reciprocal of the product of the three constants Knet, Cproj, Ceng. The upstream lemma cmin_pos states: if all three constants are strictly positive then cmin > 0. The local setting is the CPM-standalone layer that deliberately omits domain-specific material.
proof idea
The tactic proof first obtains the conjunction 0 < toyModel.C.Knet ∧ 0 < toyModel.C.Cproj ∧ 0 < toyModel.C.Ceng by simp [toyModel]. It then invokes the lemma cmin_pos (C := toyModel.C) on this hypothesis to conclude the target inequality.
why it matters
The result supplies the final conjunct in the existential witness inside CPMMethodCert.verified_any, which in turn is used by methodReport to confirm the certificate. It closes the consistency check for the CPM assumptions without reference to the forcing chain, phi-ladder, or mass formulas. The certificate as a whole records that the generic defect and energy inequalities hold and that the positivity hypotheses are realizable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.