CPMClosureCert
plain-language theorem explainer
The CPMClosureCert structure supplies a standalone certificate for CPM method closure that certifies generic A/B/C consequences together with a toy-model witness of consistency. URC adapter authors cite it to obtain quick, #eval-friendly verification strings. The definition is a one-line wrapper that delegates the verified predicate directly to CPMMethodCert.verified.
Claim. Let $C$ be the structure CPMClosureCert. Its verification predicate holds if and only if the standalone CPMMethodCert verifies, i.e., when the toy model with all functionals equal to the constant 1 satisfies the required numerical inequalities.
background
The module URCGenerators.CPMClosureCert defines a standalone certificate for the CPM method. It certifies the generic A/B/C consequences of the CPM assumptions and supplies a toy-model witness that those assumptions are consistent; the construction is deliberately #eval-friendly through a URC adapter. The local setting is the CPM Closure Certificate (Standalone) section, which records that the certificate is self-contained and does not rely on additional design choices beyond the meta-realization axioms. Upstream, the declaration depends on the structure 'for' from UniversalForcingSelfReference, which records the structural properties required of any meta-realization instance, and on CPMMethodCert, whose doc-comment states it is a 'Standalone certificate for the CPM method' whose toy model sets all functionals to 1 and checks the inequalities numerically.
proof idea
The verified field is introduced as a one-line wrapper that expands to CPMMethodCert.verified {}. The companion theorem verified_any is proved by a two-step tactic: dsimp on the definition of verified, followed by exact application of CPMMethodCert.verified_any {}.
why it matters
CPMClosureCert supplies the certificate object consumed by the downstream URC adapters CPMClosureReport.cpm_closure_ok and cpm_closure_report, which produce the success strings asserting 'CPM Closure: COMPLETE'. It therefore closes the generic CPM A/B/C certification step inside the Recognition Science URCGenerators layer while remaining consistent with the universal forcing self-reference axioms. The construction touches the open question of whether the toy-model witness can be lifted to a full non-constant model without altering the verified predicate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.