Jlog_eq_cosh
plain-language theorem explainer
The lemma states that the log-domain cost Jlog at real argument t equals cosh t minus one. Calibration researchers cite this identity when normalizing the second derivative of J at zero to enforce unit scale. The proof is a direct one-line term application of the prior unfolding lemma that rewrites Jlog via Jcost composed with exp.
Claim. For every real number $t$, $J_ {log}(t) = cosh(t) - 1$.
background
Jlog is defined as the composition Jcost(exp t), placing the cost function in logarithmic coordinates. The Calibration module proves that the second derivative of Jlog at zero equals one, fixing the scale and completing the characterization of J under the unit normalization axiom A4. Upstream, the lemma Jlog_as_cosh establishes the identity by unfolding Jlog and Jcost, rewriting with the definition of cosh and exponential identities, then closing with ring.
proof idea
The proof is a one-line term wrapper that directly invokes Jlog_as_cosh at the supplied t. That upstream lemma unfolds the definitions of Jlog and Jcost, applies the hyperbolic cosine identity together with exp_neg and inv_eq_one_div, then finishes with the ring tactic.
why it matters
This identity is used by the downstream lemma hasDerivAt_Jlog_new to show that the derivative of Jlog equals sinh t. It supports the calibration step that sets the second derivative at zero to one, thereby enforcing axiom A4. The result aligns with the J-uniqueness property (T5) in the forcing chain, where J takes the form (x + x^{-1})/2 - 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.