rsConeRecord
plain-language theorem explainer
rsConeRecord supplies the concrete numerical values for the CPM constants record in the Recognition Science cone model, setting Knet to 1, Cproj to 2, Ceng and Cdisp to 1, and cmin to 1/2. Researchers instantiating the abstract Coercive Projection Method inequalities in the Law of Existence module cite this record to fix the cone-specific normalizations. The definition is a direct record construction whose only non-trivial step is a norm_num verification that the supplied cmin matches the product formula.
Claim. The RS cone constants record is the structure with $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$, $c_{min}=1/2$, together with provenance strings for each constant.
background
The LawOfExistence module supplies a domain-agnostic formalization of the Coercive Projection Method in three parts: the projection-defect inequality, coercivity factorization via energy gap, and an aggregation principle that local tests imply global membership. CPMConstantsRecord is the structure that packages the five numerical constants together with their source attributions. The upstream definition cmin computes the coercivity threshold as the reciprocal of the product Knet · Cproj · Ceng; the fundamental tick is the RS-native time quantum equal to 1.
proof idea
The definition directly constructs the record by assigning the five numerical fields and the three provenance strings, then discharges the single consistency obligation cmin_consistent by the norm_num tactic.
why it matters
This record fixes the numerical normalizations required to instantiate the abstract CPM A/B/C logic for the RS cone geometry. It aligns with the eight-tick octave of the forcing chain (T7) and supplies the concrete values that downstream coercivity and defect bounds in the same module will use. No open questions are attached; the definition simply closes the constant interface for cone-specific applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.