pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.CPM.Examples

show as:
view Lean formalization →

The CPM.Examples module supplies concrete models that instantiate the generic Coercive Projection Method (CPM) from the LawOfExistence import. It includes the trivial model where all functionals return zero to show the inequalities hold vacuously, plus subspace, RS cone, and eight-tick models. Researchers working on Recognition Science cite these to confirm the projection-defect and coercivity predicates apply in specific cases. The module structure consists of direct model definitions followed by immediate checks against the CPM predicates.

claimThe module defines models such as the trivial model where all functionals satisfy $f(x)=0$, so that the CPM projection-defect inequality holds vacuously, together with the eight-tick model aligned to period $2^3$ and the RS-cone model.

background

This module operates inside the Coercive Projection Method (CPM) framework supplied by the imported LawOfExistence module. That module gives a generic, domain-agnostic formalization of CPM in three parts: A: Projection-Defect inequality, B: Coercivity factorization (energy gap controls defect), and C: Aggregation principle (local tests imply membership). The examples module imports this core and adds concrete models to test the predicates. The local theoretical setting is the Recognition Science derivation of physics from one functional equation, using RS-native units with $c=1$, $G=phi^5/pi$, and the eight-tick octave.

proof idea

This is a definition module with no proofs. It consists of model definitions (trivialModel, subspaceModel, rsConeModel, eightTickModel) each followed by direct verification that the CPM predicates from LawOfExistence are satisfied for that model.

why it matters in Recognition Science

The module earns its place by providing test cases that validate the CPM core from LawOfExistence, which underpins the Recognition Science forcing chain (T0-T8) and Recognition Composition Law. It supports downstream checks of the phi-ladder and eight-tick structures without introducing new theorems.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)