deriv2_Jlog
plain-language theorem explainer
The lemma states that the second derivative of the log-domain cost Jlog equals cosh. Calibration researchers cite it to normalize curvature before evaluating at zero. The proof is a short tactic sequence that substitutes the first-derivative lemma and invokes the known derivative of sinh.
Claim. $ (Jlog)''(t) = cosh t $, where $ Jlog(t) := Jcost(e^t) $ and $ Jcost(x) = (x + x^{-1})/2 - 1 $.
background
Jlog is the log-domain cost defined by composing Jcost with the exponential map, equivalently Jlog(t) = cosh(t) - 1. The Calibration module proves the second derivative of Jlog at zero equals 1, establishing the unit normalization axiom (A4) that fixes the scale of J uniquely. The upstream lemma deriv_Jlog already shows that the first derivative of Jlog is sinh.
proof idea
The tactic proof first obtains deriv Jlog = sinh by function extensionality applied to the prior lemma deriv_Jlog. It then rewrites the goal and applies the standard derivative of sinh at the point t.
why it matters
The result is invoked by the theorem Jlog_second_deriv_at_zero, which concludes that the second derivative at zero equals 1 and thereby completes axiom A4. This step anchors the Recognition Science forcing chain by fixing the curvature scale of the cost function, consistent with the RCL and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.