coneConstants
The declaration supplies the canonical RS-native constants for the cone projection in the Coercive Projection Method by setting Knet to 1, Cproj to 2, Ceng to 1 and Cdisp to 1. Researchers working on abstract coercivity models in CPM cite this instantiation to populate the generic Constants structure for downstream calculations such as cmin. The definition constructs the record directly and discharges the four non-negativity obligations via norm_num.
claimThe RS-native cone projection constants are the tuple with $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, $C_{disp}=1$, each satisfying the non-negativity conditions $0≤K_{net}$, $0≤C_{proj}$, $0≤C_{eng}$, $0≤C_{disp}$.
background
The Constants structure is the abstract bundle of four real-valued CPM parameters (Knet, Cproj, Ceng, Cdisp) together with proofs of their non-negativity. This module supplies a domain-agnostic formalization of the Coercive Projection Method in three parts: projection-defect inequality, coercivity factorization in which the energy gap controls defect mass, and aggregation of local tests into membership. The upstream Constants definition supplies the record type that coneConstants populates with the RS-specific numerical values.
proof idea
The definition directly constructs the Constants record by assigning the four numerical fields and applies norm_num to each of the four non-negativity proofs.
why it matters in Recognition Science
This supplies the concrete constants that downstream results such as cone_cmin_consistent and rs_cone_cmin_value rely on to obtain cmin = 1/2, and that rsConeModel and rsConeModel_pos instantiate for explicit coercivity checks. It anchors the RS cone model inside the abstract CPM A/B/C logic and supplies the values used by the J-cost normalization hook in the same module.
scope and limits
- Does not derive the numerical values from the Recognition Science forcing chain or RCL.
- Does not assign physical units or interpretations to the four parameters.
- Does not extend the constants to projection geometries other than the cone case.
- Does not perform symbolic refinement of Ceng or Cdisp beyond the fixed values chosen here.
Lean usage
example : cmin coneConstants = 1/2 := by simp [cone_cmin_consistent]formal statement (Lean)
206def coneConstants : Constants := {
proof body
Definition body.
207 Knet := 1,
208 Cproj := 2,
209 Ceng := 1,
210 Cdisp := 1,
211 Knet_nonneg := by norm_num,
212 Cproj_nonneg := by norm_num,
213 Ceng_nonneg := by norm_num,
214 Cdisp_nonneg := by norm_num
215}
216