hasDerivAt_Jlog_zero
plain-language theorem explainer
The lemma establishes that Jlog has derivative zero at the origin. Researchers verifying stationary points of the log-domain cost in Recognition Science would cite this when confirming the minimum at the identity. The proof is a one-line wrapper that specializes the general derivative formula for Jlog at t=0.
Claim. Let $Jlog(t) := Jcost(e^t)$. Then $Jlog$ satisfies $HasDerivAt Jlog 0 0$, i.e., its derivative at the origin is zero.
background
In the Cost module the function Jlog is defined by composing the base cost with the exponential: Jlog(t) = Jcost(exp t). This shifts the cost into logarithmic coordinates where the Recognition Science J-function takes the explicit form cosh(t) - 1. The upstream lemma hasDerivAt_Jlog states that the derivative of Jlog at any real t equals sinh(t), obtained by rewriting Jlog pointwise as cosh(t) - 1 and invoking the standard derivative of cosh.
proof idea
The proof is a one-line wrapper that applies hasDerivAt_Jlog at the concrete argument 0. Because sinh(0) equals zero, simplification immediately yields HasDerivAt Jlog 0 0.
why it matters
This result feeds the subsequent lemma deriv_Jlog_zero that extracts the explicit derivative value zero. It supplies the local verification that the log-domain cost is stationary at the origin, consistent with the symmetry built into the J-uniqueness step of the forcing chain. The declaration closes a small but necessary differentiability fact required for later minimum and averaging arguments in the Cost module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.