cproj_from_J_second_deriv
plain-language theorem explainer
The result fixes the cone projection constant at 2 once the J-cost second derivative in logarithmic coordinates is normalized to 1 at the origin. Researchers applying the Coercive Projection Method to rank-one bounds in Recognition Science cite it to obtain the optimal constant in the Hermitian inequality. The proof is a direct term pairing of reflexivity on the coneConstants definition with the pre-proved normalization lemma.
Claim. $C_ {proj} = 2$ and $d^2/dt^2 (J(e^t))|_{t=0} = 1$, where $J$ denotes the J-cost function and the second derivative condition supplies the normalization for the rank-one bound.
background
The module LawOfExistence formalizes the Coercive Projection Method in three abstract parts: projection-defect inequalities, coercivity factorization via energy gaps, and aggregation of local tests. coneConstants is the record that sets K_net = 1, C_proj = 2, C_eng = 1 and C_disp = 1 for intrinsic cone projections, keeping other constants symbolic for later domain instantiation. The J-cost function satisfies J(x) = (x + x^{-1})/2 - 1; its composition with the exponential map yields the normalized second derivative at zero that appears in the log-coordinate statement.
proof idea
The proof is a term-mode pair. Reflexivity discharges the equality C_proj = 2 directly from the definition of coneConstants. The second conjunct is supplied verbatim by the lemma Jcost_log_second_deriv_normalized, which rewrites the composed function as (e^t + e^{-t})/2 - 1 and computes its second derivative at zero by successive differentiation.
why it matters
The declaration supplies the concrete normalization required for the Hermitian rank-one bound inside the CPM projection-defect step. It anchors the constant C_proj = 2 for cone projections, consistent with J-uniqueness in the forcing chain and the eight-tick octave through the logarithmic coordinate choice. No downstream theorems are recorded yet, so the result remains a foundational hook for later aggregation and energy-gap arguments in the Law of Existence module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.