Jcost_log_second_deriv_normalized
plain-language theorem explainer
The lemma shows that the second derivative at zero of Jcost composed with the exponential equals one. Uniqueness theorems for the cost function and the Coercive Projection Method cite this normalization to fix the Hermitian projection constant at two. The proof substitutes the closed-form expression for Jcost, differentiates the resulting expression twice via HasDerivAt rules for the exponential, and evaluates at the origin.
Claim. $ (d^2/dt^2) [Jcost(e^t)]_{t=0} = 1 $
background
The Law of Existence module formalizes the Coercive Projection Method through projection-defect inequalities, coercivity factorization, and aggregation. Jcost is the function on positive reals given by Jcost(x) = (x + x^{-1})/2 - 1, which satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The lemma records the calibration condition in logarithmic coordinates. It relies on the upstream lemma Jcost_exp that supplies the explicit identity Jcost(exp t) = (exp t + exp(-t))/2 - 1 and on standard differentiability of the exponential.
proof idea
The proof equates the target composition to the explicit f(t) = (e^t + e^{-t})/2 - 1 via Jcost_exp. It derives the first derivative (e^t - e^{-t})/2 by applying HasDerivAt for addition, scaling by 1/2, and composition with negation. The second derivative at zero is then obtained by repeating the differentiation on this expression, which simplifies to (e^0 + e^0)/2 = 1 after evaluation and cancellation of the constant term.
why it matters
This normalization supplies the calibration hypothesis in Jcost_is_calibrated and Jcost_regularity_cert, which feed the axiom-free uniqueness theorem unique_cost_on_pos_from_rcl on the RCL surface. It also directly yields Cproj = 2 in cproj_eq_two_from_J_normalization and cproj_from_J_second_deriv. Within the framework the result anchors the T5 J-uniqueness step that forces the self-similar fixed point phi and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.