hasDerivAt_sinhDivAlpha
plain-language theorem explainer
The lemma establishes that the map s ↦ sinh(α s)/α has derivative cosh(α t) at any real t when α ≠ 0. Analysts verifying calibration invariance of rescaled cost functionals under coordinate change in Recognition Science would cite it. The proof composes the standard derivative of sinh with the chain rule for multiplication by α, then divides the result by the constant α.
Claim. For any real number $α ≠ 0$ and any real $t$, the function $s ↦ sinh(α s)/α$ has derivative $cosh(α t)$ at the point $s = t$.
background
In the WLOG α=1 module the calibrated cost family takes the form F_α(x) = (1/α²)(cosh(α ln x) − 1) for α ≥ 1, equivalently (1/α²) J(x^α) where J(x) = (x + x^{-1})/2 − 1. The Calibration axiom requires that if G(t) = F(exp t) then G''(0) = 1; this lemma supplies the first-derivative ingredient needed to evaluate the second derivative of the rescaled CostAlphaLog. Upstream CostAxioms.Calibration states: “Axiom 3 (Calibration): The second derivative at the origin (in log coordinates) equals 1. Let G(t) = F(exp(t)). Then G''(0) = 1.”
proof idea
The proof obtains the derivative of sinh(α s) at t by composing hasDerivAt_sinh (α t) with hasDerivAt_alpha_mul α t, which inserts a factor of α. It then converts the result to the quotient by the constant α via div_const and simplifies the field expression.
why it matters
This lemma is invoked by the downstream costAlphaLog_unit_curvature theorem, which concludes that the second derivative of CostAlphaLog α at 0 equals 1 for every α ≠ 0. The result therefore confirms calibration invariance under rescaling and justifies the WLOG reduction to α = 1. It aligns with J-uniqueness (T5) and the self-similar fixed-point forcing (T6) in the Recognition Science chain, ensuring the unit-curvature condition is independent of the multiplicative coordinate choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.