pith. sign in
module module high

IndisputableMonolith.URCGenerators.CPMMethodCert

show as:
view Lean formalization →

The CPMMethodCert module supplies a standalone certificate for the Coercive Projection Method by importing its generic A/B/C formalization. Downstream URC adapters and closure certificates cite it to verify consistency via toy-model witnesses. The module organizes definitions of a toy model together with positive assertions on defect and energy positions.

claimThe module certifies the generic Coercive Projection Method (CPM) with parts A (projection-defect inequality), B (coercivity factorization), and C (aggregation principle), witnessed by a toy model.

background

The module imports IndisputableMonolith.CPM.LawOfExistence, whose doc-comment states: 'This module provides a generic, domain-agnostic formalization of the Coercive Projection Method (CPM) in three parts (A/B/C): A: Projection-Defect inequality, B: Coercivity factorization (energy gap controls defect), C: Aggregation principle (local tests imply membership)'. This supplies the theoretical setting for the URCGenerators domain. The module itself acts as the certificate container, exposing sibling definitions such as toyModel and its positive lemmas.

proof idea

This is a definition module, no proofs. It aggregates the imported LawOfExistence structure with local toy-model constructions and positive assertions on defect position, energy position, and cmin position.

why it matters in Recognition Science

The module feeds the parent certificates in IndisputableMonolith.URCAdapters.CPMReports (machine-readable checks and pretty printers) and IndisputableMonolith.URCGenerators.CPMClosureCert (standalone CPM A/B/C consequences plus toy-model witness). It supplies the generic CPM certificate required by those downstream modules in the Recognition Science framework.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)