deriv_klQuadratic_zero
plain-language theorem explainer
The derivative of the KL quadratic approximation vanishes at equilibrium. Researchers comparing Recognition Science's J-cost to variational free energy would cite this to confirm first-order agreement in the local expansion. The proof is a one-line wrapper that extracts the derivative from the hasDerivAt property of klQuadratic at zero.
Claim. Let $k(u)$ denote the quadratic approximation to the KL divergence in log-ratio coordinates induced by the J-cost. Then $k'(0) = 0$.
background
The FEP Bridge from J-Cost module compares Recognition Science's reciprocal cost $J(x) = (x + x^{-1})/2 - 1$ with Friston-style variational free energy. In log-ratio coordinates $x = e^u$ this becomes $J(e^u) = cosh(u) - 1$. The function klQuadratic supplies the local quadratic contact between this J-cost and the KL geometry of FEP. The module states that this contact is exact at the level of value, first derivative, and second derivative at equilibrium. Upstream structures include the J-cost definition from PhiForcingDerived and the differentiability statement hasDerivAt_klQuadratic.
proof idea
This is a one-line wrapper that applies the derivative extraction from (hasDerivAt_klQuadratic 0).deriv and simplifies the result.
why it matters
The declaration confirms first-order matching between the RS J-cost and FEP KL at equilibrium, completing the local contact step of the bridge. It directly supports the sibling claim that the second derivative equals 1 and the later result jcost_kl_same_second_order_at_equilibrium. The module marks this as the theorem-grade portion of the FEP bridge while leaving Markov blankets and full Bayesian filtering for future work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.