Jcost_as_composition
plain-language theorem explainer
The lemma equates the multiplicative cost Jcost(x) to the log-domain version Jlog applied to the natural logarithm of x, for all positive reals x. Researchers deriving convexity properties or domain switches in the Recognition Science cost functions would cite this equivalence to move results between multiplicative and additive settings. The term-mode proof unfolds the definition of Jlog and cancels the exponential against the logarithm via the standard Real.exp_log identity.
Claim. For all $x > 0$, $J(x) = Jlog(log x)$, where $J(x) = (x + x^{-1})/2 - 1$ and $Jlog(t) := J(x)$ with the argument replaced by $e^t$.
background
The Cost.Convexity module proves strict convexity of the J-function on the positive reals and on the reals. Jcost is the base cost function $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Jlog is defined by composition as $Jlog(t) = J(e^t)$, which is also equal to $cosh(t) - 1$. The local setting is the preparation of these convexity facts as input to the J-uniqueness result T5 in the forcing chain. The lemma depends on the Jlog definition in the Cost module and on the real-analysis fact that $exp(log x) = x$ when $x > 0$.
proof idea
The proof is a one-line wrapper. It unfolds the definition of Jlog, which expands to Jcost composed with exp, then applies congruence to reduce the goal to $exp(log x) = x$. The final step invokes the standard lemma Real.exp_log on the hypothesis $x > 0$ and takes the symmetric form.
why it matters
The equivalence supplies the domain bridge needed for the convexity arguments that support T5 J-uniqueness in the forcing chain. It lets convexity established in the additive log domain transfer directly to the multiplicative cost domain. No downstream uses are recorded in the current graph, but the lemma closes a notational gap inside the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.