hasDerivAt_Jlog_new
plain-language theorem explainer
The lemma shows that Jlog, the logarithmic form of the Recognition cost function, has derivative sinh t at every real t. Researchers calibrating the J-cost in the phi-ladder framework cite this when computing first derivatives for normalization axioms. The short tactic proof rewrites Jlog via its cosh equivalence and invokes the standard derivative of cosh.
Claim. Let $J_{log} : ℝ → ℝ$ be defined by $J_{log}(t) = cosh t - 1$. Then the derivative of $J_{log}$ at any real $t$ equals $sinh t$.
background
In the Cost.Calibration module the function Jlog is introduced as the composition Jcost(exp t), placing the cost in logarithmic coordinates. The module proves the unit normalization axiom A4 by establishing that the second derivative of Jlog at zero equals 1. The upstream lemma Jlog_eq_cosh states that Jlog(t) equals cosh(t) minus one, which supplies the closed-form identity required for differentiation.
proof idea
The tactic first proves pointwise equality Jlog = fun s => cosh s - 1 by applying Jlog_eq_cosh at each s. It then rewrites the goal and invokes the standard fact that the derivative of cosh at t is sinh t, subtracting the constant 1.
why it matters
This lemma supplies the first-derivative step that feeds the sibling result deriv_Jlog, which in turn supports the second-derivative calibration establishing axiom A4. It completes the local analytic characterization of Jlog needed for the phi-ladder mass formulas and the eight-tick octave. The proof is closed; no scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.