deriv2_Jlog
plain-language theorem explainer
The lemma establishes that the second derivative of the log-domain cost Jlog equals the hyperbolic cosine for any real argument. Researchers calibrating the Recognition Science cost function cite it to confirm the curvature identity needed for unit normalization. The proof is a short tactic sequence that first substitutes the known first derivative sinh and then applies the standard derivative of sinh.
Claim. For every real number $t$, the second derivative of the log-domain cost function $Jlog$ satisfies $Jlog''(t) = cosh(t)$.
background
Jlog is defined by composing the base cost Jcost with the exponential: Jlog(t) := Jcost(exp t). An equivalent explicit form is (exp(t) + exp(-t))/2 - 1. The module proves calibration properties of this function, specifically that its second derivative at zero equals 1, which fixes the scale and completes the characterization of J under axiom A4. The result depends on the prior lemma that the first derivative of Jlog is sinh.
proof idea
The proof first proves deriv Jlog = sinh by function extensionality applied to the earlier result deriv_Jlog. It rewrites the target second-derivative expression with this equality, then concludes by invoking the known derivative of sinh at the arbitrary point t.
why it matters
This lemma is the direct input to the calibration theorem Jlog_second_deriv_at_zero, which states that the second derivative at zero equals 1 and thereby establishes the unit normalization axiom A4. It confirms the hyperbolic structure of the cost function, aligning with the J-uniqueness step in the forcing chain. The result closes the local characterization of curvature in the cost module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.