cost_alpha_rescaling
plain-language theorem explainer
The rescaling identity equates the alpha-parameterized cost F_alpha(x) to (1/alpha squared) times J of x to the alpha for positive real x. Researchers reducing general alpha cases to the canonical J-cost in the Recognition Science framework cite this result. The proof is a term-mode one-liner that unfolds the cost definitions and applies the core cosh-to-Jcost identity.
Claim. For real numbers $alpha$ and $x > 0$, the alpha-parameterized cost satisfies $F_alpha(x) = (1/alpha^2) J(x^alpha)$, where $F_alpha(x) := (1/alpha^2)(cosh(alpha ln x) - 1)$ and $J(y) := (y + y^{-1})/2 - 1$.
background
The module develops the without-loss-of-generality reduction to alpha equals one for calibrated cost functions after fixing unit curvature. CostAlpha defines the alpha-parameterized cost in multiplicative coordinates by CostAlpha alpha x := CostAlphaLog alpha (log x), which expands to (1/alpha squared) times (cosh(alpha times log x) minus 1). CostAlphaLog supplies the logarithmic version: (1/alpha squared) times (cosh(alpha t) minus 1). The upstream identity cosh(alpha log x) minus 1 equals Jcost of (x to the alpha) for x positive follows from the exponential definition of the power and the relation Jcost composed with exp equals cosh minus 1. This setting shows that alpha merely reparametrizes the multiplicative coordinate on positive reals without introducing new structure.
proof idea
The proof is a term-mode one-liner. It unfolds the definitions of CostAlpha and CostAlphaLog, reduces by congruence, and invokes the upstream theorem cosh_log_eq_jcost_rpow alpha x hx to finish.
why it matters
This theorem supplies the rescaling component of the WLOG alpha equals one proposition. It is used directly by cost_alpha_one_eq_jcost to recover J at alpha equals one and by wlog_alpha_eq_one to assemble the full statement that every calibrated cost is equivalent to J under coordinate rescaling. In the Recognition Science framework it supports reduction to the J-uniqueness case while preserving the unit-curvature condition G''(0) equals 1 for every alpha.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.