hasDerivAt_Jlog
plain-language theorem explainer
The lemma establishes that the derivative of the log-domain cost function at any real number t equals sinh(t). Researchers working on differentiation within the cost axioms of Recognition Science would cite this. The proof reduces the log-domain cost to cosh minus one and invokes the known derivative of the hyperbolic cosine.
Claim. For all real numbers $t$, if $J(t) := Jcost(e^t)$, then the derivative of $J$ at $t$ is $sinh(t)$.
background
The module develops the log-domain cost by composing the base cost function with the exponential map. The log-domain cost is defined as the base cost applied to exp(t). This provides the setting for differentiation in log coordinates, as required by the cost axioms that identify J with the base cost. An upstream result supplies a parallel derivative statement, while the free-energy bridge uses this to show that the second derivative of the log-domain cost at zero equals one.
proof idea
The tactic proof cites the derivative of cosh at t, which is sinh(t). Subtracting the constant one preserves the derivative. It then proves that the log-domain cost equals the function cosh minus one by applying extensionality and simplifying the definition using the expression for the base cost and the identity for negative exponentials. Substitution of this equality yields the result.
why it matters
This lemma is invoked to obtain the derivative of the averaged log cost under averaging derivations and the zero case at equilibrium. It supports the J equals base cost axiom and the theorem establishing that the derivative of the derivative of the log-domain cost at zero is one. In the Recognition framework it enables the transition to logarithmic coordinates that aligns with the J-uniqueness property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.