Jlog_second_deriv_at_zero
plain-language theorem explainer
The calibration result establishes that the second derivative of the log-domain cost function Jlog at the origin equals one. Researchers calibrating the Recognition Science cost function would cite this to anchor the unit normalization axiom. The proof reduces the claim via the known second-derivative formula for Jlog and evaluates the hyperbolic cosine at zero.
Claim. $ (d^2 / dt^2) J_{log}(t) |_{t=0} = 1 $, where $ J_{log}(t) := J_{cost}(e^t) $.
background
Jlog is the log-domain version of the cost function, defined by composing Jcost with the exponential: Jlog(t) = Jcost(exp t), which equals cosh(t) - 1. The module proves the second derivative of Jlog at zero equals 1, establishing the unit normalization axiom (A4) that fixes the scale uniquely and completes the characterization of J. The key upstream lemma states that the second derivative of Jlog equals the hyperbolic cosine function.
proof idea
The proof applies the lemma that the second derivative of Jlog equals cosh, reducing the claim directly to the evaluation cosh(0) = 1.
why it matters
This result feeds the theorems Jcost_comp_exp_second_deriv_at_zero and Jlog_unit_curvature in the same module. It establishes the unit normalization axiom (A4) as described in the module documentation. In the Recognition Science framework this calibration anchors the J function's curvature at the identity, consistent with J-uniqueness and the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.