Pith. sign in
module module high

IndisputableMonolith.CPM.LawOfExistence

show as:
view Lean formalization →

Bundles the coercive projection method (CPM) constants and the elementary defect-energy inequalities that turn a cost gap into a quantitative existence lower bound. Physicists working on ILG, mass ladders, or the T0–T8 forcing chain cite it for the shared (K_net, C_proj, C_eng, c_min) package. The module is mostly definitions plus short comparison lemmas; no deep uniqueness argument lives here.

claimPackage of CPM constants $(K_{\mathrm{net}}, C_{\mathrm{proj}}, C_{\mathrm{eng}})$ with $c_{\min}=1/(K_{\mathrm{net}} C_{\mathrm{proj}} C_{\mathrm{eng}})>0$, together with the model inequalities $\mathrm{defect}\le C\cdot\mathrm{energyGap}$ and $\mathrm{energyGap}\ge c_{\min}\cdot\mathrm{defect}$, and the cone specialization $K_{\mathrm{net}}=1$, $C_{\mathrm{proj}}=2$.

background

CPM (coercive projection method) is the quantitative layer that sits on the Recognition cost $J$. After the cost foundation fixes $J(x)=(x+x^{-1})/2-1$ on $\mathbb{R}_+$, one still needs constants that convert an abstract defect (distance to a constraint set or orthocomplement) into an energy gap measured by $J$. This module is the abstract bundle of those constants.

It imports the Cost library and exposes a Constants record, the derived coercivity floor $c_{\min}$, positivity of $c_{\min}$, and a Model interface that packages the comparison lemmas defect ≤ constants · energyGap and the reverse energyGap ≥ c_min · defect. A cone specialization records the RS-native values $K_{\mathrm{net}}=1$ and $C_{\mathrm{proj}}=2$ used by the projection certificates downstream.

Notation is deliberately domain-agnostic: the same constant package is later instantiated for ILG gravity, CPT cores, and the verification certificates that prove the constants are computed rather than assumed.

proof idea

Definition module with short comparison lemmas, not a deep proof development. Constants and Model are structure/record bundles. c_min is the reciprocal product $1/(K_{\mathrm{net}} C_{\mathrm{proj}} C_{\mathrm{eng}})$; cmin_pos is immediate positivity from positive factors. The defect/energyGap lemmas are one-line rearrangements of the Model inequalities. Cone lemmas simply plug in the RS values $K_{\mathrm{net}}=1$, $C_{\mathrm{proj}}=2$ and discharge the resulting equalities by rfl or norm_num-style arithmetic.

why it matters in Recognition Science

This is the shared constant spine for the whole CPM stack. CostUniqueness (T5 J-uniqueness) and UnifiedForcingChain (T0–T8 from the cost foundation) import it so the forcing chain can quote a single c_min package. Downstream verification certificates CminDerivationCert, CprojDerivationCert, and KnetDerivationCert prove the numerical values are derived from J-normalization rather than postulated; CPMBridge.Initiality uses the cone values $(K_{\mathrm{net}},C_{\mathrm{proj}})=(1,2)$ as the unique RS witness. ILG.CPMInstance and CPT.Core instantiate the same Model for gravity and discrete CPT cores. Without this bundle every certificate would redefine the constant algebra ad hoc.

scope and limits

used by (8)

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 (29)