cost_alpha_one_eq_jcost
plain-language theorem explainer
Setting the rescaling parameter to one recovers the canonical J-cost exactly on positive reals. Researchers working on coordinate calibration in Recognition Science cite this to reduce the general α-family to the standard J case. The proof substitutes into the rescaling identity and simplifies the resulting power term.
Claim. For every $x > 0$, the cost function $F_1(x)$ equals the J-cost $J(x)$.
background
The module shows that after unit-curvature calibration the family takes the form $F_α(x) = (1/α²)(cosh(α ln x) - 1)$ for α ≥ 1. The rescaling identity states that this equals $(1/α²) J(x^α)$, where $J(y) = (y + y^{-1})/2 - 1$. Setting α = 1 therefore recovers J exactly. The upstream rescaling theorem supplies the general identity via the relation cosh(α log x) - 1 = J(x^α).
proof idea
One-line wrapper that applies the rescaling identity cost_alpha_rescaling at α = 1 and then uses simp to reduce the power x^1 to x.
why it matters
This supplies the recovery step inside wlog_alpha_eq_one and feeds directly into alpha_pinned_to_one_implies_J and the full uniqueness theorem J_uniquely_calibrated_via_higher_derivative. It confirms that the bilinear cost reduces to J under unit-curvature calibration, aligning with J-uniqueness (T5) in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.