hasDerivAt_costAlphaLog_fourth
plain-language theorem explainer
The lemma establishes that the fourth derivative of the α-parameterized cost G_α(t) equals α² cosh(α t) for any α ≠ 0. Calibration theorists cite it when separating bilinear branches by higher-order invariants after the second-derivative calibration has been fixed to 1. The proof rewrites via the third-derivative identity then composes the chain rule for sinh with constant multiplication and ring simplification.
Claim. Let $G_α(t) := (1/α²)(cosh(α t) - 1)$. Then the fourth derivative satisfies $d⁴G_α/dt⁴(t) = α² cosh(α t)$.
background
The Alpha-Coordinate Fixation module works inside the one-parameter family obtained from branch selection: G_α(t) = (1/α²)(cosh(α t) - 1), equivalently F_α(x) = (1/α²)(cosh(α ln x) - 1) for α ≥ 1. The second derivative G_α''(t) = cosh(α t) yields the invariant G_α''(0) = 1 independent of α. The upstream lemma deriv_deriv_deriv_costAlphaLog_eq supplies the third derivative α sinh(α t). This derivative calculus sits inside the broader Recognition Science reduction of calibrated costs to the J-automorphism family.
proof idea
The tactic proof first rewrites the target using the third-derivative equality deriv_deriv_deriv_costAlphaLog_eq. It constructs the inner derivative HasDerivAt (fun x => α x) α t from hasDerivAt_id and mul_const, then composes with hasDerivAt_sinh to obtain the derivative of sinh(α s). Constant multiplication by α produces the final expression, which is converted and simplified by ring.
why it matters
The result feeds the downstream theorem costAlphaLog_fourth_deriv_at_zero, which evaluates the fourth derivative at zero to α² and thereby forces α = 1 under the calibration condition G^(4)(0) = 1. It realises Option 2 (higher-derivative calibration) from the branch-selection paper, isolating the canonical J-cost via the relation cost_alpha_one_eq_jcost. Within the framework it closes the T5 J-uniqueness step after the second-derivative invariance has been established.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.