pith. sign in
module module moderate

IndisputableMonolith.URCAdapters.CPMReports

show as:
view Lean formalization →

Module supplies #eval-friendly reports confirming the standalone CPM method certificate. It lets users verify generic A/B/C consequences for any CPM model plus assumption consistency via toy witness. Structure consists of one import plus sibling report definitions.

claimStandalone CPM certificate report: generic A/B/C consequences available for any Model $M$, assumptions consistent as witnessed by concrete toy model.

background

Upstream CPMMethodCert supplies a standalone certificate that avoids domain or problem-specific material. It certifies that generic CPM A/B/C consequences hold for any CPM Model and that the assumptions remain consistent, witnessed by a concrete toy model. This adapter module exposes those certifications through directly evaluable report objects.

proof idea

This is a definition module, no proofs. It imports the certificate module and defines report functions for evaluation.

why it matters in Recognition Science

Supports confirmation of the standalone CPM certificate. Feeds the URCAdapters domain by making the generic properties from CPMMethodCert directly accessible for verification.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (2)