Jcost_satisfies_composition_law
plain-language theorem explainer
Jcost satisfies the Recognition Composition Law, the functional equation F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y) for x, y > 0. Researchers proving uniqueness of the cost functional under T5 would cite this as the verification step for the candidate J. The proof is a one-line term that invokes the equivalence to the cosh-add identity and applies the direct algebraic check for Jcost.
Claim. The function $J : (0,∞) → ℝ$ defined by $J(x) = (x + x^{-1})/2 - 1$ satisfies $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ for all $x, y > 0$.
background
The Cost Uniqueness module consolidates results to prove that any cost functional obeying symmetry, unit normalization, strict convexity, and calibration equals Jcost on the positive reals. The Recognition Composition Law is the property that a function F satisfies F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y) for all positive x and y. The upstream theorem composition_law_equiv_coshAdd states that this law on F is equivalent to the cosh-add identity G(s+t) + G(s-t) = 2G(s)G(t) + 2G(s) + 2G(t) after the change of variables x = e^s, y = e^t with G(t) = F(e^t). Jcost is the explicit function that also equals cosh(log x) - 1.
proof idea
The proof is a one-line term application of the right-to-left direction of composition_law_equiv_coshAdd to Jcost, followed by the theorem Jcost_cosh_add_identity. That identity is verified by direct expansion: substitute the definition of Jcost, use exp(t+u) = exp(t)exp(u) and exp(t-u) = exp(t)/exp(u), then simplify the resulting hyperbolic expressions.
why it matters
This result verifies that the candidate cost Jcost obeys the Recognition Composition Law, a required property in the T5 uniqueness theorem of the Cost Uniqueness module. It closes one leg of the forcing chain landmark T5 J-uniqueness and supports the main claim that symmetry, normalization, convexity, and calibration force the cost to be J. The declaration sits between the functional-equation lemmas and the full uniqueness statement T5_uniqueness_complete.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.