cone_Cproj_eq_two
plain-language theorem explainer
The projection constant in the RS-native cone model is fixed at 2. Coercivity calculations in the CPM framework cite this normalization when deriving the minimal coercivity constant of 1/2. The equality holds by direct reflexivity on the constant definition.
Claim. In the RS-native constants for cone projection, the projection factor satisfies $C_{proj} = 2$.
background
The Law of Existence module develops an abstract Coercive Projection Method with three components: projection-defect inequalities, coercivity factorization via energy gaps, and aggregation of local tests. The coneConstants definition supplies the RS-native values Knet = 1, Cproj = 2, Ceng = 1, Cdisp = 1, keeping other parameters symbolic. This lemma records the fixed projection constant used throughout the CPM coercivity calculations.
proof idea
The proof applies reflexivity directly to the definition of coneConstants, which hardcodes the projection constant as 2.
why it matters
This result supplies the normalization required for theorems establishing that the coercivity constant cmin equals 1/2 in the RS cone model. It appears in downstream derivations in ConstantsAudit and Examples modules. The value connects to the J-normalization condition in the Recognition Science framework, where the derivative of the J-cost function at zero fixes the Hermitian projection constant at 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.