Jlog
plain-language theorem explainer
The log-domain cost is obtained by composing the base J-cost with the exponential map. Analysts working on stationary points and minima for the Recognition Science energy functional cite this construction when shifting to additive coordinates. It is supplied as a direct composition of the imported Jcost with the real exponential.
Claim. Define the log-domain cost by $J_ {log}(t) := J_{cost}(e^t)$ for real $t$.
background
Jcost is the Recognition Science cost function Jcost(x) = (x + x^{-1})/2 - 1 for x > 0, equivalently cosh(log x) - 1. The FlogEL module performs cost analysis after the change of variables that converts the original multiplicative scale into an additive log scale. The definition draws on the Jcost supplied by the parent Cost module and the cosh-form expression already recorded in the Jlog submodule.
proof idea
This is a one-line definition that applies Jcost directly to exp t. No lemmas or tactics are invoked.
why it matters
The definition supplies the function used by all derivative and minimality results in the Cost module, including the global-minimum theorem and the stationary-point lemma at zero. It thereby supports the J-uniqueness step (T5) in the forcing chain by furnishing the log-domain tool needed for cost analysis. Downstream lemmas such as EL_global_min rely on it to conclude that Jlog(0) is the unique minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.