CPMMethodCert
CPMMethodCert supplies a bare marker type confirming consistency of the CPM coercivity and aggregation inequalities for any Model. Auditors and report generators cite it when building standalone verification layers or closure certificates. The declaration is an empty structure deriving only Repr, with consistency witnessed by the toyModel facts defined in the same module.
claimThe type $CPMMethodCert$ is a marker structure certifying that the CPM assumptions remain consistent, witnessed by a toy model in which all functionals equal 1 and the inequalities hold for constants $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$.
background
In the LawOfExistence module a Model comprises constants $C$, defectMass, orthoMass, energyGap and tests. The coercivity constant $c_{min}$ is defined as the reciprocal of the product $K_{net}·C_{proj}·C_{eng}$. Upstream results include the theorem defect_le_constants_mul_energyGap stating defectMass(a) ≤ (Knet·Cproj·Ceng)·energyGap(a) and the companion aggregation theorem defect_le_constants_mul_tests. The present module deliberately omits domain-specific material and supplies only a generic consistency witness.
proof idea
The declaration is a definition of an empty structure deriving Repr. No tactics or lemmas are applied inside the structure itself; the consistency claim is discharged by the separate toyModel lemmas (toyModel_defect_pos, toyModel_energy_pos, toyModel_cmin_pos) that inhabit the same file.
why it matters in Recognition Science
CPMMethodCert is the base certificate consumed by exampleCertificates in ConstantsAudit and by methodReport in CPMReports; it is also delegated to by CPMClosureCert. It supplies the required consistency witness for the standalone CPM layer described in the module documentation. The declaration touches the open question of extending the toy constants to physical regimes while remaining a minimal, domain-free marker.
scope and limits
- Does not model any concrete physical system or domain data.
- Does not prove the inequalities for arbitrary models beyond the toy witness.
- Does not import or depend on anthropology or astrophysics results.
- Does not compute or verify numerical values outside the fixed toy constants.
Lean usage
noncomputable def methodReport : String := let cert : CPMMethodCert := {} ; have _ : verified cert := verified_any cert ; ...formal statement (Lean)
22structure CPMMethodCert where
23 deriving Repr
24
25/-- A small toy CPM model witnessing consistency of the assumptions.
26
27All functionals are constant 1, and the inequalities hold numerically with
28`Knet = 1`, `Cproj = 2`, `Ceng = 1`, `Cdisp = 1`.
29
30This is not intended to model physics; it is only a nontrivial consistency witness.
31-/