deriv2_Jlog
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the explicit closed form of Jlog.
- Does not evaluate the second derivative at any specific numerical point.
- Does not treat complex or discrete arguments.
- Does not derive third or higher derivatives.
Lean usage
rw [deriv2_Jlog]; exact cosh_zeroformal statement (Lean)
34lemma deriv2_Jlog (t : ℝ) : deriv (deriv Jlog) t = cosh t := by
proof body
Tactic-mode proof.
35 have h1 : deriv Jlog = sinh := by
36 funext s; exact deriv_Jlog s
37 rw [h1]
38 exact (hasDerivAt_sinh t).deriv
39
40/-- The calibration theorem: second derivative at zero equals 1 -/