cone_Ceng_eq_one
plain-language theorem explainer
The lemma fixes the energy coefficient Ceng to unity inside the canonical RS cone projection constants. Coercivity calculations for cone models in the Coercive Projection Method cite this value to obtain the minimal constant cmin equal to one half. The proof is a direct reflexivity step that matches the explicit assignment in the coneConstants definition.
Claim. In the RS-native cone projection constants, the energy coefficient satisfies $C_{eng}=1$.
background
The Law of Existence module supplies an abstract Coercive Projection Method (CPM) with three parts: projection-defect inequalities, coercivity factorization controlled by energy gaps, and aggregation of local tests into global membership. The coneConstants definition supplies the canonical RS values Knet=1, Cproj=2, Ceng=1, Cdisp=1, kept symbolic for domain refinements while preserving the generic A/B/C logic.
proof idea
The proof is a one-line wrapper that applies reflexivity to the explicit value assigned to Ceng inside the coneConstants definition.
why it matters
This normalization is invoked by downstream results such as c_value_cone and cone_cmin_numerical to conclude that the RS cone coercivity constant equals 1/2. It anchors the energy scaling inside the generic CPM framework of the Law of Existence module and aligns with Recognition Science native-unit conventions that set energy-related factors to unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.