klQuadratic_zero
plain-language theorem explainer
The theorem establishes that the quadratic proxy for KL divergence vanishes at the equilibrium point in log-ratio coordinates. Researchers bridging Recognition Science to Friston's free-energy principle would cite this when verifying local consistency between J-cost and variational free energy. The proof is a one-line simplification that unfolds the definition of the quadratic proxy.
Claim. The local quadratic proxy for the KL divergence in one log-ratio coordinate satisfies $u^2/2$ evaluated at $u=0$ equals zero.
background
The module provides the first Lean anchor comparing Recognition Science to Friston-style free-energy-principle mechanics. Recognition Science uses the reciprocal J-cost $J(x)=(x+x^{-1})/2-1$, which in log-ratio coordinates $x=exp u$ becomes $cosh u-1$. The local quadratic proxy is defined as $klQuadratic(u):=u^2/2$, matching the second-order Taylor contact with KL geometry at equilibrium. Upstream, the equilibrium theorem states that J-cost at 1 equals zero, corresponding to $u=0$.
proof idea
The proof is a one-line wrapper that applies simplification on the definition of klQuadratic.
why it matters
This anchors the local value-level agreement between Recognition Science J-cost and FEP variational free energy at equilibrium. It fills the theorem-grade part of the FEP bridge module and marks the exact quadratic contact before higher structure such as Markov blankets is addressed. The module notes that full derivation of Bayesian filtering from the Recognition Composition Law remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.