c_value_cone
Researchers applying the Coercive Projection Method in Recognition Science cite this result to fix the normalized coercivity constant for the cone projection case. It states that c_min of the RS cone constants equals one half. The proof is a direct term-mode simplification that unfolds the cmin definition, substitutes the three cone component lemmas, and reduces the arithmetic by norm_num.
claimFor the cone projection constants with $K_{net}=1$, $C_{proj}=2$, and $C_{eng}=1$, the coercivity constant satisfies $c_{min}=1/2$.
background
The module supplies an abstract formalization of the Coercive Projection Method with three parts: A the projection-defect inequality, B the coercivity factorization in which the energy gap bounds the defect, and C the aggregation principle that local tests imply global membership. The cmin definition records the coercivity constant as the reciprocal of the product $K_{net}·C_{proj}·C_{eng}$. The coneConstants record instantiates these values as 1, 2, and 1 for the RS-native cone case, accompanied by separate lemmas that each component equals its assigned number.
proof idea
One-line wrapper that applies simp to unfold cmin together with the three cone component equalities, then reduces the resulting rational expression by norm_num.
why it matters in Recognition Science
The theorem supplies the concrete normalization required by the formal constants record in the Law of Existence module, completing the cone case for the abstract CPM framework. It directly supports the coercivity factorization step (part B) and supplies the value used when domain-specific instantiations later refine the placeholders for C_eng and C_disp.
scope and limits
- Does not prove the inequality for arbitrary positive constants.
- Does not derive the component values from a deeper principle.
- Does not instantiate the constants for any concrete physical domain.
formal statement (Lean)
359theorem c_value_cone : cmin RS.coneConstants = 1/2 := by
proof body
Term-mode proof.
360 simp only [cmin, RS.cone_Knet_eq_one, RS.cone_Cproj_eq_two, RS.cone_Ceng_eq_one]
361 norm_num
362
363end Bridge
364
365/-! ## Formal Constants Record
366
367A structured record of all CPM constants with their derivations,
368suitable for auditing and JSON export. -/
369
370/-- Complete record of CPM constants with provenance. -/