hasDerivAt_deriv_Jlog_zero
plain-language theorem explainer
The second derivative of the log-coordinate reciprocal cost equals one at the equilibrium point zero. Researchers bridging Recognition Science to Friston's free-energy principle cite this for the exact local Fisher curvature match. The proof first equates the first derivative of Jlog to sinh via the known derivative lemma, then invokes the standard derivative of sinh at zero.
Claim. $tmapsto (d/dt)J_{log}(t)$ has derivative $1$ at $t=0$, where $J_{log}(t)=cosh(t)-1$.
background
The log-coordinate J-cost is defined by $J_{log}(t):=J(exp t)$ where $J(x)=(x+x^{-1})/2-1$ is the reciprocal cost. This yields the closed form $J_{log}(t)=cosh t-1$. The module establishes a local bridge to Friston's free-energy principle by showing that this cost shares value, first derivative, and second derivative with the KL quadratic at the equilibrium point $t=0$ (see MODULE_DOC). Upstream results include the lemma hasDerivAt_Jlog asserting HasDerivAt Jlog (sinh t) t, which follows from the chain rule on the composition with the exponential and the known derivative of cosh.
proof idea
The proof first proves that the derivative of Jlog equals the hyperbolic sine function by applying the derivative of the known hasDerivAt_Jlog lemma pointwise via funext. It then rewrites the goal with this identification and applies the standard Real.hasDerivAt_sinh at zero.
why it matters
This result supplies the second-derivative match required by the parent theorem jcost_kl_same_second_order_at_equilibrium, which states that Jlog and klQuadratic agree through second order at equilibrium. It completes the local crossover between the Recognition Science reciprocal cost and FEP-style variational free energy, as described in the module documentation. The bridge remains local and does not yet derive Markov blankets from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.