Jlog
plain-language theorem explainer
J_log(t) is defined to be (exp(t) + exp(-t))/2 - 1. Workers on the Euler-Lagrange analysis in the Recognition framework cite this definition when shifting the cost to logarithmic coordinates. The definition is a direct one-line expression that agrees with the composition of the base J-cost and the exponential map.
Claim. The log-domain cost function is defined by the formula $J_ {log}(t) = (e^t + e^{-t})/2 - 1$ for all real $t$.
background
The base J-cost satisfies J(x) = (x + x^{-1})/2 - 1 for x > 0 and obeys the Recognition Composition Law. The log-domain version is obtained by composition: J_log(t) := J(exp t). This permits additive analysis of the cost functional. The upstream definition in FlogEL states: Log-domain cost: Jcost composed with exp.
proof idea
The declaration supplies a direct definition using the exponential function. It matches the composition form Jcost(exp t) from the parent Cost module. No lemmas or tactics are invoked; the body is the explicit algebraic expression.
why it matters
Downstream results such as deriv_Jlog_zero, EL_global_min, and hasDerivAt_Jlog apply this definition to locate the stationary point at zero and establish the global minimum. It realizes the J-uniqueness step T5 of the forcing chain in logarithmic variables, written as cosh(t) - 1, and supports the transition to the phi fixed point and eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.