CostAlpha
plain-language theorem explainer
CostAlpha defines the α-parameterized cost in multiplicative coordinates as F_α(x) = (1/α²)(cosh(α ln x) − 1) for x > 0. Researchers proving coordinate rescaling in the Recognition Science framework cite it when reducing the bilinear family to the canonical J-cost. The definition is a one-line wrapper that applies CostAlphaLog to the natural logarithm.
Claim. The α-parameterized cost is $F_α(x) = (1/α²)(cosh(α ln x) − 1)$ for $x > 0$.
background
The WLOG α = 1 module explores the family of solutions F_α after the unit-curvature calibration κ(F) = 1 forces c = 2α². CostAlphaLog supplies the additive version G_α(t) = (1/α²)(cosh(α t) − 1). CostAlpha substitutes t = ln x to obtain the multiplicative form. Upstream Jcost is recovered exactly when α = 1, and the map x ↦ x^α is a group automorphism of (ℝ₊, ·).
proof idea
CostAlpha is defined directly as CostAlphaLog α (log x). This is a one-line wrapper that applies the log-coordinate cost to the multiplicative input.
why it matters
The definition supplies the multiplicative form used by AlphaCoordinateFixationCert and the theorems alpha_pinned_to_one_implies_J and J_uniquely_calibrated_via_higher_derivative. It feeds cost_alpha_rescaling and wlog_alpha_eq_one, which together establish that every calibrated F_α reduces to J under rescaling. In the framework this closes the α-freedom after T5 J-uniqueness, fixing the coordinate so that D = 3 and the alpha band can be read off without extra parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Multidimensional cost geometry
"J(x₁,...,xₙ) = ½(R + R⁻¹) − 1 with R = ∏xᵢ^αᵢ; in logarithmic coordinates J(t) = cosh(Σαᵢtᵢ) − 1."