toyModel_energy_pos
plain-language theorem explainer
The toy CPM model has a strictly positive energy gap. Researchers verifying consistency of the CPM assumptions would cite this to confirm the witness satisfies energy positivity. The proof is a direct simplification that unfolds the toyModel definition and checks the resulting inequality.
Claim. For the toy model, the energy gap exceeds zero: $energyGap(toyModel) > 0$.
background
The module certifies generic CPM A/B/C consequences for any Model and consistency via a toy model. The toyModel definition sets all functionals to constant 1 with Knet = 1, Cproj = 2, Ceng = 1, Cdisp = 1; it serves solely as a nontrivial consistency witness rather than a physical model. Energy gap is defined as the excess energy above the Newtonian ground state, given by the integral of (∇w)² plus potential terms. This lemma is part of the standalone CPM certificate layer. The upstream energyGap declaration states: 'Energy gap: excess energy above the Newtonian ground state. Proportional to the integral of (∇w)² + potential terms.'
proof idea
This is a one-line wrapper proof that applies simp using the toyModel definition to reduce the inequality to a numerical check that holds.
why it matters
The lemma contributes to the CPMMethodCert by supplying a positive energy witness, which the methodReport invokes to confirm the certificate. It closes the consistency check for the toy model in the URCGenerators layer. This supports the broader claim that CPM assumptions are consistent without domain-specific material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.