deriv_deriv_deriv_costAlphaLog_eq
plain-language theorem explainer
The third derivative of the α-parameterized cost G_α(t) = (1/α²)(cosh(α t) − 1) equals the function α sinh(α t) for α ≠ 0. Researchers extending unit-curvature calibration to higher orders in Recognition Science branch selection would cite this when preparing the fourth-derivative condition that pins α. The proof is a one-line wrapper that applies the hasDerivAt version of the third derivative pointwise and extracts the derivative value.
Claim. Let $G_α(t) := (1/α²)(cosh(α t) − 1)$ for real α ≠ 0. Then the third derivative satisfies $d³G_α/dt³ = α sinh(α t)$.
background
The AlphaCoordinateFixation module works inside the one-parameter family obtained from branch selection, where the log-coordinate cost is G_α(t) = (1/α²)(cosh(α t) − 1). This family satisfies G_α''(0) = 1 for every α, so second-derivative calibration alone cannot fix α; the module therefore turns to higher derivatives. The definition of this cost is taken from the WLOGAlphaOne companion, which also supplies the first two derivatives.
proof idea
The proof is a one-line wrapper. It uses funext to reduce the functional equality to a pointwise statement, then calls (hasDerivAt_costAlphaLog_third α hα t).deriv to read off the derivative value from the already-established HasDerivAt fact.
why it matters
This result supplies the third-derivative expression required by the immediate successor hasDerivAt_costAlphaLog_fourth, which in turn yields the fourth derivative α² cosh(α t) whose value at zero forces α = 1. That step completes Option 2 (higher-derivative calibration) of the branch-selection paper, isolating the canonical J-cost J(x) = (x + x⁻¹)/2 − 1. The lemma therefore sits inside the forcing chain that reduces the bilinear branch to the unique self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.