deriv_costAlphaLog_eq
plain-language theorem explainer
This lemma gives the explicit first derivative of the α-parameterized cost function G_α(t) = (1/α²)(cosh(α t) - 1) as sinh(α t)/α for α ≠ 0. Researchers establishing curvature invariance under coordinate rescaling in the WLOG α = 1 proposition cite it. The proof is a one-line term that applies function extensionality to the hasDerivAt_costAlphaLog fact.
Claim. For α ≠ 0, the derivative of G_α(t) := (1/α²)(cosh(α t) - 1) equals the function t ↦ sinh(α t)/α.
background
The WLOGAlphaOne module develops the coordinate-rescaling proposition: after calibration κ(F) = 1 forces c = 2α², the family F_α(x) = (1/α²)(cosh(α ln x) - 1) for α ≥ 1 satisfies F_α(x) = (1/α²) · J(x^α) where J is the Recognition Science cost. The function CostAlphaLog α t is defined as (1/α²)(cosh(α t) - 1) and supplies the equivalent representation in additive log coordinates.
proof idea
The proof is a term-mode one-liner: funext reduces the equality of functions to a pointwise statement, then the .deriv projection is applied to the HasDerivAt fact returned by hasDerivAt_costAlphaLog α hα t.
why it matters
It is invoked by costAlphaLog_unit_curvature to obtain G_α''(0) = 1 independently of α, and by results in AlphaCoordinateFixation. The lemma therefore closes the step that justifies setting α = 1 without loss of generality, recovering the J-cost exactly and aligning with the self-similar fixed point (T5-T6) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.