wlog_alpha_eq_one
plain-language theorem explainer
The declaration shows that any α-parameterized cost F_α coincides with the canonical J-cost after rescaling the input by α and dividing by α². Researchers deriving the Recognition Science cost functions from the functional equation would invoke this result to reduce all cases to α = 1. The proof is a term-mode tuple that directly assembles four supporting lemmas without further reasoning.
Claim. For any real number α > 0, let F_α(x) = (1/α²)(cosh(α ln x) − 1) for x > 0 be the α-parameterized cost and let J(y) = (y + y⁻¹)/2 − 1 be the canonical cost. Then F_α(x) = (1/α²) J(x^α) for x > 0, F_1(x) = J(x) for x > 0, (xy)^α = x^α y^α for x, y > 0, and the second derivative of G_α(t) = (1/α²)(cosh(α t) − 1) at t = 0 equals 1.
background
The module develops the coordinate-rescaling proposition for the calibrated cost family after the calibration condition κ(F) = 1 forces c = 2α². CostAlphaLog α t is defined as (1/α²)(cosh(α t) − 1), the cost expressed in logarithmic coordinates. CostAlpha α x applies this definition to log x, producing F_α(x) = (1/α²)(cosh(α ln x) − 1) in multiplicative coordinates. The module documentation states that the family is F_α(x) = (1/α²)(cosh(α ln x) − 1) for α ≥ 1 and that the map x ↦ x^α is a group automorphism of the positive reals under multiplication. Upstream results supply the rescaling identity (cost_alpha_rescaling), the recovery at α = 1 (cost_alpha_one_eq_jcost), the multiplicative homomorphism (rpow_mul_hom'), and the unit-curvature theorem (costAlphaLog_unit_curvature) asserting that the second derivative of CostAlphaLog α at 0 is always 1.
proof idea
The proof is a term-mode tuple that directly invokes four lemmas. The first conjunct applies cost_alpha_rescaling α x hx. The second applies cost_alpha_one_eq_jcost x hx. The third applies rpow_mul_hom' α hx hy. The fourth applies costAlphaLog_unit_curvature α hα.ne'.
why it matters
This theorem justifies the without-loss-of-generality reduction to α = 1 in the Recognition Science derivation of the cost function. It supports the J-uniqueness step (T5) by showing that α merely reparametrizes the multiplicative coordinate without introducing new structure. The module documentation concludes that setting α = 1 recovers J exactly and that the unit-curvature condition G_α''(0) = 1 holds independently of α. The result is fully proved with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.