cone_Knet_eq_one
plain-language theorem explainer
The lemma fixes the net constant Knet to one inside the RS cone projection constants. Workers on the Coercive Projection Method cite it when normalizing the abstract CPM model before computing coercivity bounds. The proof is a direct reflexivity step on the definition of coneConstants.
Claim. In the RS-native CPM constants for cone projection, the net constant satisfies $K_{net}=1$.
background
The Law of Existence module supplies an abstract Coercive Projection Method (CPM) in three layers: projection-defect inequality, coercivity factorization via energy gap, and aggregation from local tests. coneConstants records the canonical RS values with Knet set to 1, Cproj to 2, Ceng to 1 and Cdisp to 1, keeping Ceng and Cdisp symbolic for later domain refinement. The upstream definition states that these are placeholders for the cone projection case and that domain instantiations may refine them.
proof idea
One-line wrapper that applies reflexivity to the field assignment Knet := 1 inside the coneConstants definition.
why it matters
This supplies the Knet value required by downstream results such as c_value_cone and rs_cone_cmin_value, which conclude that the coercivity constant cmin equals 1/2 for the RS cone model. It completes the normalization step for the cone constants inside the Law of Existence module and supports the abstract CPM logic that connects to the eight-tick net and D=3 spatial structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.