CPMConstantsRecord
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prescribe numerical values for any constant.
- Does not prove that the constants are positive.
- Does not derive K_net or C_proj from the forcing axioms.
- Does not contain the projection-defect or energy-gap statements themselves.
formal statement (Lean)
371structure CPMConstantsRecord where
372 /-- Net/covering constant -/
373 Knet : ℝ
374 /-- Projection constant -/
375 Cproj : ℝ
376 /-- Energy control constant -/
377 Ceng : ℝ
378 /-- Dispersion constant -/
379 Cdisp : ℝ
380 /-- Coercivity constant c_min -/
381 cmin : ℝ
382 /-- Derivation source for K_net -/
383 Knet_source : String
384 /-- Derivation source for C_proj -/
385 Cproj_source : String
386 /-- Consistency check: c_min = 1/(K_net · C_proj · C_eng) -/
387 cmin_consistent : cmin = (Knet * Cproj * Ceng)⁻¹
388
389/-- RS cone constants record. -/