hasDerivAt_costAlphaLog_first
plain-language theorem explainer
The lemma states that the first derivative of the α-parameterized cost G_α(t) = (1/α²)(cosh(α t) - 1) equals sinh(α t)/α at any t, for α ≠ 0. Researchers formalizing higher-derivative calibration to fix the branch parameter α in Recognition Science would cite it when deriving the sequence of derivatives needed for fourth-order pinning. The proof is a direct computation that composes the derivative of cosh with the linear map α t, subtracts the constant, multiplies by 1/α², and simplifies algebraically to the target expression.
Claim. Let $G_α(t) := (1/α²)(cosh(α t) - 1)$ for $α ≠ 0$. Then $G_α'(t) = sinh(α t)/α$.
background
In the Alpha-Coordinate Fixation module the branch-selection theorem reduces the calibrated bilinear branch to the one-parameter family $F_α(x) = (1/α²)(cosh(α ln x) - 1)$ with $α ≥ 1$. The function CostAlphaLog α t is defined as $(1/α²)(cosh(α t) - 1)$, the log-coordinate version $G_α(t)$. The module explores higher-derivative calibration to pin α, noting that the second derivative at zero is 1 independently of α while the fourth is α². This lemma supplies the first derivative, which is used to derive the higher ones. It relies on the definition of CostAlphaLog from the WLOGAlphaOne module together with standard real-analysis facts for the derivative of cosh and linear maps.
proof idea
The proof first obtains the derivative of the inner map x ↦ α x by applying hasDerivAt_id, mul_const, and mul_comm. It then composes with hasDerivAt_cosh to differentiate cosh(α s), subtracts the constant 1, multiplies the result by the constant 1/α², unfolds the definition of CostAlphaLog, and finishes with field_simp to reach sinh(α t)/α.
why it matters
This lemma supports the chain of derivative computations that culminate in the fourth derivative of G_α at zero equaling α²; under the calibration G^{(4)}(0) = 1 this forces α = 1 and isolates the canonical J-cost. It contributes to Option 2 of the three candidate α-fixation routes listed in the companion paper RS_Branch_Selection.tex. In the Recognition framework the result helps enforce J-uniqueness (T5) by selecting the self-similar fixed point through higher-order calibration of the cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.