hasDerivAt_deriv_klQuadratic_zero
plain-language theorem explainer
The theorem proves that the second derivative of the KL quadratic at equilibrium equals 1. Researchers comparing Recognition Science's J-cost to Friston's free-energy principle would cite it for the exact local curvature match. The proof first shows that the first derivative of klQuadratic is the identity function via pointwise application of hasDerivAt_klQuadratic, then evaluates the derivative of that identity at zero.
Claim. The second derivative of the KL quadratic function at the equilibrium point satisfies $d^2/du^2$ klQuadratic$(u)|_{u=0} = 1$.
background
In the FEP Bridge module the reciprocal J-cost of Recognition Science is J(x) = (x + x^{-1})/2 - 1; under the change of variables u = log x this becomes cosh(u) - 1. The sibling definition klQuadratic supplies the quadratic form that reproduces the Fisher information geometry of variational free energy at equilibrium. The module documentation states that the local quadratic contact between these two costs is exact through second order at u = 0.
proof idea
The proof constructs the equality deriv klQuadratic = fun u => u by applying the derivative operator to the result of hasDerivAt_klQuadratic at each point. It then rewrites the target HasDerivAt expression with this equality and reduces it to the standard fact that the derivative of the identity function at zero is 1.
why it matters
This declaration supplies the second-derivative leg of the local crossover between J-cost and KL geometry, directly feeding the downstream theorem jcost_kl_same_second_order_at_equilibrium that equates value, first derivative and second derivative. The module positions the result as the theorem-grade anchor for the FEP bridge while noting that Markov blankets and full Bayesian filtering remain outside its scope. It therefore closes one concrete link in the comparison of Recognition Science cost functions with variational free energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.