hasDerivAt_costAlphaLog_third
plain-language theorem explainer
The lemma asserts that the third derivative of the α-parameterized cost G_α(t) = (1/α²)(cosh(α t) − 1) equals α sinh(α t) at every real t when α ≠ 0. Workers on higher-order calibration in the branch-selection setting cite it to extend the second-derivative identity toward the α-pin. The proof rewrites via the second-derivative lemma, applies the chain rule to cosh composed with the linear map x ↦ α x, and normalizes by ring.
Claim. Let $G_α(t) := (1/α²)(cosh(α t) − 1)$. Then the third derivative satisfies $d³G_α/dt³(t) = α sinh(α t)$.
background
The module develops higher-derivative conditions that fix the branch parameter α in the one-parameter family obtained from branch selection. CostAlphaLog α is the map t ↦ (1/α²)(cosh(α t) − 1), the log-coordinate form of the calibrated cost F_α(x) = (1/α²)(cosh(α ln x) − 1). Its second derivative is cosh(α t), so the curvature at zero is 1 for every α, as recorded by the upstream lemma deriv_deriv_costAlphaLog_eq.
proof idea
The proof first rewrites the second derivative by calling deriv_deriv_costAlphaLog_eq. It then constructs HasDerivAt for the linear map x ↦ α x by scaling the identity map, composes with hasDerivAt_cosh via the chain rule, and finishes with convert and ring to obtain the target expression α sinh(α t).
why it matters
The result supplies the third-derivative formula required by the immediate downstream lemma deriv_deriv_deriv_costAlphaLog_eq, which in turn yields the fourth-derivative identity used to force α = 1. That step closes Option 2 of the higher-derivative calibration route in the branch paper, isolating the canonical J-cost inside the T5–T6 forcing chain of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.