Jlog_as_cosh
plain-language theorem explainer
The identity equates the log-domain cost Jlog(t) to cosh(t) minus one. Cost-layer derivations in Recognition Science cite it to obtain closed forms for derivatives and convexity checks. The term proof reduces the claim by unfolding the exponential composition and normalizing the hyperbolic definition via ring.
Claim. For all real $t$, the log-domain cost $Jlog(t) := Jcost(e^t)$ equals $cosh(t) - 1$.
background
The Cost module defines the base cost Jcost satisfying the Recognition Composition Law. Jlog is introduced as the pullback Jlog(t) := Jcost(exp t) to work in additive log coordinates. This matches the direct definition ((exp t + exp(-t))/2) - 1 given in the sibling Jlog submodule. The upstream result J_eq_Jcost links this to the foundation J function used in the forcing chain.
proof idea
Unfold Jlog and Jcost to substitute the composition. Rewrite with the exponential form of cosh, replace the reciprocal by division, negate the exponent, and finish with ring arithmetic.
why it matters
Downstream lemmas such as hasDerivAt_Jlog and Jcost_exp_cosh apply this identity directly. It supplies the log_closed_form field in the public_cost_layer theorem. The result realizes the J-uniqueness step (T5) of the UnifiedForcingChain by expressing the cost as cosh(log x) - 1, which underpins the phi-ladder and the alpha band constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.