costAlphaLog_unit_curvature
plain-language theorem explainer
costAlphaLog_unit_curvature shows that the second derivative at zero of the α-parameterized log-cost G_α(t) = (1/α²)(cosh(α t) - 1) equals one for every nonzero real α. Workers on the WLOG reduction for calibrated costs in Recognition Science cite it to confirm invariance under rescaling. The term-mode proof substitutes the first-derivative formula and evaluates the derivative of sinh(αt)/α at the origin.
Claim. For every real α ≠ 0, if G_α(t) = (1/α²)(cosh(α t) - 1), then the second derivative of G_α at t = 0 equals 1.
background
The module develops the coordinate-rescaling argument that reduces every calibrated cost to the canonical J-cost. CostAlphaLog α is the function G_α(t) := (1/α²)(cosh(α t) - 1) representing the cost after the multiplicative change of variable x ↦ x^α. The upstream lemma deriv_costAlphaLog_eq states that the first derivative of CostAlphaLog α equals the map t ↦ sinh(α t)/α. The Calibration axiom requires that the second derivative of any admissible cost at the origin equals 1, normalizing curvature so that the solution family is unique up to reparametrization.
proof idea
The proof applies the equality from deriv_costAlphaLog_eq to replace the outer derivative, then invokes the derivative of the sinh-division expression at argument zero supplied by hasDerivAt_sinhDivAlpha. The resulting expression simplifies via mul_zero to a multiple of cosh(0), which equals 1.
why it matters
The result is invoked inside wlog_alpha_eq_one to establish the fourth conjunct of the WLOG statement, confirming that every member of the calibrated family satisfies the unit-curvature axiom. It directly supports the module conclusion that α merely reparametrizes the multiplicative group without introducing new cost structures, aligning with J-uniqueness in the forcing chain. No open scaffolding remains for this invariance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.