hasDerivAt_costAlphaLog
plain-language theorem explainer
The lemma establishes that the α-parameterized cost in logarithmic coordinates, G_α(t) = (1/α²)(cosh(α t) - 1), has derivative sinh(α t)/α at any real t when α ≠ 0. Analysts reducing the Recognition Science cost functions to the α = 1 case would cite this result to confirm differentiation commutes with the rescaling. The proof is a direct term-mode calculation that chains the derivative of cosh through the linear map α t, subtracts the constant, scales by the prefactor 1/α², and simplifies.
Claim. Let α ∈ ℝ with α ≠ 0 and t ∈ ℝ. The function G_α(t) := (1/α²)(cosh(α t) - 1) satisfies HasDerivAt G_α (sinh(α t)/α) t.
background
The module develops the without-loss-of-generality reduction to α = 1 after the calibration κ(F) = 1 forces c = 2α². In this setting the α-parameterized cost in log coordinates is defined by CostAlphaLog α t := (1/α²)(cosh(α t) - 1), which is the reparametrization of F_α(x) = (1/α²)(cosh(α ln x) - 1) under the substitution t = ln x. The module document states that the map x ↦ x^α is a group automorphism of the positive reals, so α merely reparametrizes the multiplicative coordinate while preserving the unit-curvature condition G_α''(0) = 1.
proof idea
The term proof first obtains the derivative of cosh(α s) at s = t by composing hasDerivAt_cosh with hasDerivAt_alpha_mul. It subtracts the constant 1, multiplies the result by the constant function 1/α², and simplifies the zero terms that appear. After unfolding CostAlphaLog the expression is converted to the target and cleaned with field_simp.
why it matters
This lemma supplies the explicit derivative required by the downstream result deriv_costAlphaLog_eq, which in turn supports the WLOG α = 1 proposition in the DAlembert module. It confirms that differentiation respects the α-rescaling of the J-cost, thereby underpinning the T5 J-uniqueness step and the claim that every α yields a valid unit-curvature solution. The result closes a technical gap in the coordinate-rescaling argument without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.