deriv_costAlphaLog_eq
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.
claimFor α ≠ 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 in Recognition Science
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.
scope and limits
- Does not compute the second derivative of CostAlphaLog.
- Does not restrict α to positive reals.
- Does not address the multiplicative form F_α(x) directly.
- Does not treat the singular case α = 0.
Lean usage
rw [deriv_costAlphaLog_eq α hα]formal statement (Lean)
103private lemma deriv_costAlphaLog_eq (α : ℝ) (hα : α ≠ 0) :
104 deriv (CostAlphaLog α) = fun t => sinh (α * t) / α :=
proof body
Term-mode proof.
105 funext fun t => (hasDerivAt_costAlphaLog α hα t).deriv
106