deriv_costAlphaLog_eq
plain-language theorem explainer
The lemma states that the derivative of the α-parameterized cost G_α equals the map t ↦ sinh(α t)/α. Researchers extending branch selection to higher-derivative calibration cite it when differentiating the log-curvature cost to isolate α. The proof is a one-line wrapper that applies the first-derivative hasDerivAt lemma and extracts the derivative value via funext.
Claim. Let $G_α(t) := (1/α²)(cosh(α t) - 1)$ for $α ≠ 0$. Then $dG_α/dt = sinh(α t)/α$.
background
The Alpha-Coordinate Fixation module works inside the one-parameter family obtained from the branch-selection theorem: $F_α(x) = (1/α²)(cosh(α ln x) - 1)$ with $α ≥ 1$. In log coordinates this is the cost $G_α(t) = CostAlphaLog α t = (1/α²)(cosh(α t) - 1)$. The upstream lemma hasDerivAt_costAlphaLog_first already records that $G_α$ is differentiable at each $t$ with derivative value sinh(α t)/α.
proof idea
The proof is a one-line wrapper: funext fun t => (hasDerivAt_costAlphaLog_first α hα t).deriv. It lifts the pointwise HasDerivAt fact to an equality of functions.
why it matters
The result supplies the first link in the derivative chain that lets the fourth-derivative calibration force α = 1 and recover the canonical J-cost. It is invoked by hasDerivAt_costAlphaLog_second and by costAlphaLog_unit_curvature. The module document identifies this route as Option 2 from the branch paper, selected because it re-uses the existing IsCalibrated derivative framework; the generator-calibration and action-minimisation routes remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.