CPMMethodCert
plain-language theorem explainer
CPMMethodCert defines an empty structure that serves as a standalone certificate for the CPM method, confirming generic A/B/C consequences hold for any Model and that assumptions remain consistent under a toy witness with constant functionals. Researchers building URC generators or running CPM audits cite it to establish baseline consistency before domain applications. The declaration is a bare structure deriving Repr whose verification predicates are supplied separately.
Claim. A structure $CPMMethodCert$ that certifies consistency of the CPM method, witnessed by a toy model in which all functionals equal 1 and the inequalities hold numerically for $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$.
background
The CPM method is defined in LawOfExistence via a Model structure containing Constants (Knet, Cproj, Ceng, Cdisp), defectMass, orthoMass, energyGap, and tests. Key supporting results include the definition cmin(C) = 1/(Knet · Cproj · Ceng) and the theorems defect_le_constants_mul_energyGap (D ≤ (Knet Cproj Ceng)(E-E0)) and defect_le_constants_mul_tests (D ≤ (Knet Cproj Cdisp) sup T). The module supplies a domain-independent layer that certifies these consequences for arbitrary Models.
proof idea
This is a definition of an empty structure deriving Repr. No lemmas or tactics are applied; the structure acts purely as a marker type whose verification is delegated to separate predicates in downstream files.
why it matters
CPMMethodCert is referenced by CPMClosureCert (which delegates its verification predicate), exampleCertificates, and methodReport. It completes the standalone CPM layer described in the module documentation, ensuring the coercivity and aggregation links remain consistent before use in domains such as fluids or nucleosynthesis. It touches the consistency witness requirement in the Recognition framework without introducing domain-specific material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.