cone_cmin_numerical
plain-language theorem explainer
The theorem verifies that the coercivity constant c_min equals one half for the cone projection constants. CPM audit procedures cite this result to confirm numerical consistency of the derived values. The proof is a term-mode reduction that substitutes the three constant equalities and normalizes the arithmetic.
Claim. For the cone constants with $K_{net}=1$, $C_{proj}=2$, $C_{eng}=1$, the coercivity constant satisfies $c_{min}=1/2$.
background
The CPM Constants Audit module supplies machine-checkable verification that constants derived from Recognition Science invariants meet their required numerical properties. The coercivity constant is defined as the reciprocal of the product of the net kernel, projection, and energy constants: $c_{min}=(K_{net}·C_{proj}·C_{eng})^{-1}$. The coneConstants instantiation sets these to 1, 2, and 1 respectively, as established by the lemmas cone_Knet_eq_one, cone_Cproj_eq_two, and cone_Ceng_eq_one.
proof idea
The proof applies simp to unfold the definition of cmin together with the three equality lemmas for the cone constants, then invokes norm_num to evaluate the arithmetic to one half.
why it matters
This numerical check supports the consistency section in the audit report generated by printConsistency and the full JSON export in generateJSONReport. It confirms that the cone projection constants satisfy the coercivity relation required by the LawOfExistence module. Within the Recognition Science framework, such verifications close the loop on the CPM constants derived from the forcing chain invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.