c_value_cone
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.