toyModel_defect_pos
plain-language theorem explainer
The lemma establishes that defect mass is strictly positive in the toy CPM consistency model. Researchers auditing the standalone CPM certificate would cite it to confirm the witness satisfies the required deviation condition. The proof is a one-line simp wrapper that unfolds the constant-functional toy model and reduces the inequality directly from the defect mass definition.
Claim. Let $M_d$ be the defect mass of a model, defined as the squared $L^2$ deviation of the kernel from unity weighted by baryonic mass. In the toy model with all functionals constantly equal to 1, $M_d > 0$.
background
The CPM method certificate supplies a standalone verification that generic CPM A/B/C consequences hold for any model, witnessed by a concrete toy model. This toy model sets every functional to the constant 1 and satisfies the numerical inequalities with Knet = 1, Cproj = 2, Ceng = 1, Cdisp = 1; it serves only as a consistency witness, not a physical model.
proof idea
One-line wrapper that applies simp to the toy model definition, which substitutes the constant values and lets the defect mass expression evaluate to a positive quantity.
why it matters
The result feeds the methodReport (which forces evaluation of the toy witness facts) and the CPMMethodCert structure. It closes the consistency check for the CPM assumptions in the URCGenerators layer by confirming the toy model exhibits the required positive defect mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.