deriv_Jlog
plain-language theorem explainer
The lemma establishes that the first derivative of the log-domain cost function equals the hyperbolic sine. Researchers calibrating the J-cost in Recognition Science cite this identity when differentiating in logarithmic coordinates to reach the unit normalization axiom. The proof is a one-line wrapper that extracts the derivative value from the hasDerivAt fact for the rewritten cosh-minus-one form.
Claim. For every real number $t$, the derivative of the log-domain cost function at $t$ equals $sinh t$, where the log-domain cost is the composition of the base J-cost with the exponential map.
background
The Cost.Calibration module proves normalization properties of the J-cost in its logarithmic representation. The log-domain cost is defined by composing the base J-cost with the exponential, which is equivalent to the expression cosh t minus one. This representation lets the module use standard hyperbolic derivatives to fix the scale via axiom A4, which requires the second derivative at zero to equal one.
proof idea
The proof is a one-line wrapper that applies the .deriv method to the hasDerivAt_Jlog_new lemma at the point t. That upstream lemma first rewrites the log-domain cost to cosh minus one via the Jlog_eq_cosh sibling and then invokes the known derivative of cosh.
why it matters
This lemma is invoked directly by deriv2_Jlog to obtain the second derivative as cosh t, which confirms unit curvature at zero and completes axiom A4 in the calibration module. The result supports the full characterization of J required for the Recognition forcing chain, the phi-ladder mass formula, and the eight-tick octave structure that yields D equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.