cosh_log_eq_jcost_rpow
plain-language theorem explainer
The identity equates cosh(α log x) minus one to the J-cost of x raised to α for positive x. Researchers establishing the without-loss-of-generality reduction to α = 1 in the coordinate-rescaling family cite it when collapsing the general solution to the unit case. The short proof rewrites the power via the exponential definition and invokes the upstream relation between Jcost and the hyperbolic cosine.
Claim. For real α and x > 0, cosh(α log x) − 1 equals J(x^α), where J(y) = (y + y^{-1})/2 − 1 denotes the J-cost function.
background
The J-cost satisfies J(exp(t)) = cosh(t) − 1 by the upstream lemma Jcost_exp_cosh. Module WLOGAlphaOne develops the calibrated family F_α(x) = (1/α²)(cosh(α ln x) − 1) for α ≥ 1. The local proposition asserts F_α(x) = (1/α²) J(x^α), so that the map x ↦ x^α acts as a group automorphism of the positive reals and α merely reparametrizes the multiplicative coordinate.
proof idea
The tactic proof first obtains the auxiliary equality x^α = exp(α log x) by rewriting the real power definition for positive base and commuting the factors. It then substitutes this expression and applies the lemma Jcost_exp_cosh in reverse to reach the target identity.
why it matters
This supplies the algebraic step for the downstream rescaling theorem cost_alpha_rescaling, which states CostAlpha α x = (1/α²) Jcost(x^α). It directly supports the WLOG α = 1 conclusion after calibration forces c = 2α², placing the result inside the forcing chain at J-uniqueness (T5) and the self-similar fixed point (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.