Jcost_comp_exp_second_deriv_at_zero
plain-language theorem explainer
The theorem establishes that the second derivative at zero of Jcost composed with the exponential equals one. Researchers calibrating the Recognition Science cost function cite this to enforce unit normalization. The proof rewrites the composition to Jlog by definition and invokes the matching result for Jlog.
Claim. $ (d^2 / dt^2) [Jcost(e^t)]|_{t=0} = 1 $
background
Jlog is defined by Jlog(t) := Jcost(Real.exp t), shifting the cost function into logarithmic coordinates. The module proves that the second derivative of Jlog at zero equals 1, which is the unit normalization axiom A4 fixing the scale of J uniquely. This rests on the upstream theorem Jlog_second_deriv_at_zero, which reduces the claim via the explicit form of Jlog to the known value cosh(0) = 1.
proof idea
The proof records that the map t ↦ Jcost(Real.exp t) equals Jlog by definition, rewrites the expression, and applies Jlog_second_deriv_at_zero directly.
why it matters
This supplies the concrete witness that Jcost satisfies the UnitCurvature class, which packages the calibration axiom. It is invoked in the instance for UnitCurvature Jcost and appears in the proof of defect_eq_ortho_of_subspace_case inside LawOfExistence. The result completes the local characterization of J by enforcing unit curvature at the identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.