Jcost_log_second_deriv_normalized
plain-language theorem explainer
The second derivative at the origin of J composed with the exponential equals one. Uniqueness results for the cost function and CPM projection constants cite this log-coordinate normalization to fix calibration. The tactic proof rewrites the composition to an explicit form using Jcost_exp then applies repeated HasDerivAt rules for exponentials, negation, and scaling to evaluate the second derivative at zero.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Then the second derivative satisfies $d^2/dt^2 [J(e^t)]|_{t=0} = 1$.
background
The CPM.LawOfExistence module formalizes the generic Coercive Projection Method in three abstract parts: projection-defect inequality, coercivity factorization via energy gaps, and aggregation of local tests. J-cost is introduced via the explicit identity Jcost(exp t) = ((exp t + exp(-t))/2) - 1 supplied by the upstream lemma Jcost_exp. The local setting records normalizations that serve as justification hooks for downstream uniqueness statements on the RCL surface.
proof idea
The proof introduces an auxiliary f equal to the explicit hyperbolic expression of Jcost(exp t). It derives the first derivative by chaining HasDerivAt_exp, hasDerivAt_neg, addition, and mul_const. It then rewrites the first-derivative function and repeats the HasDerivAt steps at the point zero, using exp_zero to obtain the value 1 before rewriting back through the original equality.
why it matters
This normalization is invoked by Jcost_is_calibrated and Jcost_regularity_cert to support the axiom-free uniqueness theorem unique_cost_on_pos_from_rcl. It directly justifies the Hermitian constant C_proj = 2 in cproj_eq_two_from_J_normalization and cproj_from_J_second_deriv. Within the framework it closes the T5 J-uniqueness step by fixing the second log-derivative, consistent with the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.