hasDerivAt_klQuadratic
plain-language theorem explainer
The theorem states that the derivative of the KL quadratic at any real point u equals u itself. Researchers comparing Recognition Science's J-cost to Friston's free-energy principle cite this result when verifying local agreement between the two geometries through first order. The proof is a short tactic script that unfolds the definition and applies the power rule for differentiation before normalizing with ring.
Claim. Let $f(u) = u^2 / 2$. Then $f'(u) = u$ for every real $u$.
background
The module provides the first Lean anchor for comparing Recognition Science with Friston-style free-energy-principle mechanics. Recognition Science uses the reciprocal cost $J(x) = (x + x^{-1})/2 - 1$, which becomes $cosh u - 1$ when $x = exp u$. The upstream definition klQuadratic supplies the local quadratic proxy for KL divergence in one log-ratio coordinate, given explicitly by $u^2 / 2$ (doc: 'The local quadratic proxy for KL divergence in one log-ratio coordinate').
proof idea
The tactic proof unfolds klQuadratic to obtain the expression $u^2 / 2$. It then applies hasDerivAt_pow to the squaring map, yielding derivative $2u$ at the point $u$, divides the result by the constant 2, and finishes with a convert and ring normalization to match the claimed derivative value $u$.
why it matters
This result supplies the first-derivative fact required by the downstream theorems deriv_klQuadratic_zero and hasDerivAt_deriv_klQuadratic_zero. It completes the local quadratic contact step in the FEP bridge (module doc: 'the local quadratic contact with the Fisher/KL geometry is exact at the level of value, first derivative, and second derivative at equilibrium'). The module records that the construction does not yet derive Markov blankets or Bayesian filtering from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.