cproj_eq_two_from_J_normalization
plain-language theorem explainer
Under the normalization that the second derivative of Jcost composed with exp equals one at zero, the cone projection constant C_proj equals two. Researchers modeling coercive projections or Hermitian rank-one bounds in Recognition Science would cite this to fix the constant from the J-uniqueness property. The proof is a one-line simplification that invokes the reflexivity lemma for cone constants.
Claim. Assuming the second derivative of the map $tmapsto J(e^t)$ equals 1 at $t=0$, where $J$ denotes the J-cost, the projection constant $C_{proj}$ in the cone constants structure equals 2.
background
The module formalizes the Coercive Projection Method (CPM) in three abstract parts: projection-defect inequality, coercivity factorization via energy gaps, and aggregation of local tests. The Constants structure bundles four real parameters including Knet (nonnegative) and Cproj (the Hermitian rank-one projection factor). J-cost is defined via the Recognition Science functional $J(x)=(x+x^{-1})/2-1$, and the supplied hypothesis is exactly the log-coordinate normalization $J''(1)=1$ proved upstream in Jcost_log_second_deriv_normalized. coneConstants supplies the default RS-native values with Cproj preset to 2, while cone_Cproj_eq_two records this value by reflexivity.
proof idea
The proof is a one-line wrapper that applies the simp lemma cone_Cproj_eq_two. This lemma states coneConstants.Cproj=2 by rfl, discharging the goal once the J-normalization hypothesis is supplied as context.
why it matters
The declaration records the concrete value of the projection constant under the RS J-normalization, supplying the bridge between abstract CPM constants and the Recognition Science forcing chain (T5 J-uniqueness and the associated second-derivative condition). It supports the Law of Existence module's generic A/B/C logic for projection-defect inequalities without committing to domain-specific measure theory. No downstream uses are recorded yet, leaving open its integration into concrete fluid or astrophysical instantiations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.