klQuadratic
plain-language theorem explainer
klQuadratic supplies the quadratic proxy for KL divergence in log-ratio coordinates as u squared over two. Researchers bridging Recognition Science to Friston's free-energy principle cite it for the exact local match in value and derivatives at equilibrium. The definition is a direct algebraic assignment with no additional lemmas or tactics.
Claim. The function defined by $k(u) = u^2 / 2$ provides the local quadratic proxy for the Kullback-Leibler divergence in one log-ratio coordinate $u$.
background
This module anchors the comparison between Recognition Science reciprocal costs and variational free energy. The J-cost is defined as $J(x) = (x + x^{-1})/2 - 1$, which in log coordinates $x = e^u$ becomes cosh u minus 1. The quadratic proxy captures the second-order contact at equilibrium. Upstream definitions of cost from multiplicative recognizers and observer forcing supply the J-cost that this quadratic approximates locally.
proof idea
The declaration is a direct definition of the quadratic expression. No lemmas from upstream results are invoked; it encodes the Taylor approximation explicitly.
why it matters
It feeds the FEPBridgeLocalCert structure and the theorem establishing identical second-order behavior between J-cost and this quadratic at equilibrium. This marks the theorem-grade local crossover with FEP mechanics in the Recognition framework, without deriving full Markov blankets or filtering.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.