klQuadratic_zero
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive Markov blankets from the Recognition Composition Law.
- Does not address Bayesian filtering or higher-order terms beyond the quadratic.
- Does not claim global equivalence between J-cost and free energy.
formal statement (Lean)
42@[simp] theorem klQuadratic_zero : klQuadratic 0 = 0 := by
proof body
Term-mode proof.
43 simp [klQuadratic]
44
45/-- The KL quadratic has zero first derivative at equilibrium. -/