hasDerivAt_costAlphaLog_second
plain-language theorem explainer
This lemma shows that the second time derivative of the α-parameterized log-cost G_α equals cosh(α t) for α ≠ 0. Researchers calibrating higher derivatives to fix the branch parameter would cite it when isolating the canonical J-cost. The argument rewrites the first derivative explicitly then applies the chain rule to sinh composed with linear scaling, followed by constant division.
Claim. Let $G_α(t) := α^{-2}(cosh(α t) - 1)$ for real $α ≠ 0$. Then the derivative of $G_α'$ satisfies $HasDerivAt (deriv G_α) (cosh(α t)) t$ at every real $t$.
background
The Alpha-Coordinate Fixation module works inside the one-parameter family obtained from branch selection: $G_α(t) = α^{-2}(cosh(α t) - 1)$, the log-coordinate version of $F_α(x) = α^{-2}(cosh(α ln x) - 1)$. Its first derivative is already recorded as $sinh(α t)/α$ by the sibling lemma deriv_costAlphaLog_eq. The module tests higher-derivative calibration as one of three routes listed in the companion paper; the second derivative at zero is identically 1 for any α, so it supplies no pinning information.
proof idea
The proof rewrites the target via deriv_costAlphaLog_eq, then builds the inner derivative of multiplication by α from the identity map scaled by a constant (using mul_comm to reorder). It composes with the known derivative of sinh to obtain cosh(α t) · α, and finally divides by the constant α.
why it matters
This lemma is the second link in the derivative chain that reaches the fourth derivative at zero equaling α². It therefore feeds the downstream result deriv_deriv_costAlphaLog_eq and the theorem alpha_pin_under_high_calibration that forces α = 1, isolating J(x) = (x + x^{-1})/2 - 1. In the Recognition framework it realises Option 2 (higher-derivative calibration) from the branch-selection paper, complementing T5 J-uniqueness by fixing the coordinate scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.