CostAlpha
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.
claimThe α-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 in Recognition Science
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.
scope and limits
- Does not extend the domain to non-positive reals.
- Does not enforce the second-derivative calibration G''(0) = 1.
- Does not derive the value of α from higher derivatives.
- Does not prove uniqueness of the cost function among all solutions.
formal statement (Lean)
34def CostAlpha (α x : ℝ) : ℝ :=
proof body
Definition body.
35 CostAlphaLog α (log x)
36
37/-! ## Rescaling Identity -/
38
39/-- Core identity: cosh(α log x) − 1 = J(x^α) for x > 0.
40 Proof uses x^α = exp(α log x), then Jcost ∘ exp = cosh − 1. -/