CPMConstantsRecord
plain-language theorem explainer
CPMConstantsRecord packages the five real constants of the Coercive Projection Method together with provenance strings and the built-in algebraic consistency relation cmin = 1/(Knet · Cproj · Ceng). Workers on the generic CPM A/B/C logic in the Law of Existence module cite the record when instantiating concrete models such as the eight-tick or RS-cone cases. The declaration is a pure structure definition that enforces the consistency equation at the type level.
Claim. A record consisting of real numbers $K_ {net}$, $C_{proj}$, $C_{eng}$, $C_{disp}$, $c_{min}$, strings recording the derivation sources of $K_{net}$ and $C_{proj}$, and satisfying the consistency equation $c_{min} = (K_{net} · C_{proj} · C_{eng})^{-1}$.
background
The Law of Existence module supplies an abstract formalization of the Coercive Projection Method consisting of a projection-defect inequality, a coercivity factorization controlled by an energy gap, and an aggregation principle. CPMConstantsRecord serves as the common container for the numerical parameters that enter these statements. Upstream, K_net is fixed at (9/7)^2 from the eight-tick structure while C_proj is fixed at 2 as the operator-norm bound on the projection kernel. The auxiliary definition cmin computes the reciprocal product 1/(Knet · Cproj · Ceng) to avoid duplication, and Energy is identified with the real numbers in RS-native units.
proof idea
The declaration is a structure definition. It introduces the five real fields Knet, Cproj, Ceng, Cdisp, cmin, the two source strings, and the single field that asserts the equality cmin = (Knet * Cproj * Ceng)^{-1}. No lemmas are invoked and no tactics are used; the consistency constraint is enforced directly by the field type.
why it matters
The record is the immediate parent of the concrete instantiations eightTickRecord and rsConeRecord. It therefore supplies the constant data required for the eight-tick octave in the forcing chain and for the RS cone construction. By packaging the provenance strings it records the origin of K_net from the eight-tick cycle and C_proj from the CPM paper bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.