JlogDerivCert
plain-language theorem explainer
Empty audit tag whose verification predicate asserts that the log-domain cost has derivative sinh(t) at every real t. Anyone checking the calculus backbone of the J-cost (critical point, sign, monotonicity) cites this certificate. Discharge is a one-line wrapper around the existing hasDerivAt_Jlog lemma.
Claim. A certificate object $c$ is verified precisely when, for every real $t$, the log-domain cost $J_{\log}$ is differentiable at $t$ with derivative $\sinh(t)$. Equivalently: $\frac{d}{dt} J_{\log}(t) = \sinh(t)$ holds pointwise on $\mathbb{R}$.
background
In the Cost module, the log-domain cost is $J_{\log}(t) := J(e^{t})$, which equals $\cosh(t) - 1$. The ordinary J-cost is the T5 unique functional $J(x) = (x + x^{-1})/2 - 1$, so $J_{\log}$ is just that cost pulled back to additive coordinates via the exponential.
The module packages the elementary calculus identity $J_{\log}'(t) = \sinh(t)$ as an audit certificate. That identity is the bridge from the closed form to first-order analysis: $\sinh(0) = 0$ (stationary point), $\sinh$ changes from negative to positive across zero (local minimum), and $J_{\log}$ is decreasing on $(-\infty,0)$ and increasing on $(0,\infty)$.
Upstream, hasDerivAt_Jlog already proves the derivative statement by rewriting $J_{\log}$ as $\cosh - 1$ and applying Mathlib's hasDerivAt_cosh.
proof idea
The structure itself carries no data; it is a pure tag. The associated predicate verified is definitionally the universal statement $\forall t, \mathrm{HasDerivAt}, J_{\log}, (\sinh t), t$.
The companion theorem verified_any is a one-line wrapper: introduce $t$, then apply the upstream lemma hasDerivAt_Jlog t. No new analysis is performed at this layer.
why it matters
This sits in the Verification domain as a machine-checkable packaging of the first derivative of the log-domain cost. Combined with strict convexity (second-derivative or Jensen arguments elsewhere), it supplies the calculus route to uniqueness of the global minimum of $J_{\log}$ at $t = 0$, which is the additive form of the unique minimum of $J$ at $x = 1$.
That uniqueness is the analytic face of T5 J-uniqueness in the forcing chain: $J(x) = \cosh(\log x) - 1$ is forced, and the log chart makes the critical-point geometry elementary via $\sinh$. The certificate chain uses this fact for sign analysis and monotonicity before higher-level recognition-cost arguments.
No downstream consumers are recorded yet; the declaration is an audit endpoint rather than a lemma in a longer proof tree.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.