jcost_kl_same_second_order_at_equilibrium
plain-language theorem explainer
The theorem establishes that the log-domain reciprocal cost Jlog and the KL quadratic approximation agree in value, first derivative, and second derivative at the equilibrium point zero. Researchers bridging Recognition Science to Friston-style free-energy mechanics would cite this local contact result. The term-mode proof splits the conjunction, applies simplification with the Jlog zero lemma for the value, uses direct simplification for the first derivative, and rewrites the second derivatives via the pre-proved derivative facts for both maps
Claim. Let $J_ {log}(t) := cosh t - 1$ and let $klQuadratic$ be the quadratic approximation to the Kullback-Leibler divergence in log-ratio coordinates. Then $J_{log}(0) = klQuadratic(0)$, $J_{log}'(0) = klQuadratic'(0)$, and $J_{log}''(0) = klQuadratic''(0)$.
background
The module supplies the first Lean anchor comparing Recognition Science reciprocal costs with Friston-style variational free energy. The reciprocal cost is defined by $J(x) = (x + x^{-1})/2 - 1$; in log-ratio coordinates $t = log x$ this becomes $Jlog(t) = cosh t - 1$. The sibling definition klQuadratic supplies the quadratic term whose Fisher curvature matches the KL geometry at equilibrium.
proof idea
The term proof opens with constructor to split the three-way conjunction. The value equality is discharged by simp [Jlog_zero]. The first-derivative equality follows by a second simp. The second-derivative equality rewrites both sides using the derivative facts supplied by hasDerivAt_deriv_Jlog_zero and hasDerivAt_deriv_klQuadratic_zero.
why it matters
The result populates the fisher_contact field of the local FEP/RS bridge certificate fepBridgeLocalCert. It records the exact second-order agreement between the RS cost and the KL quadratic at equilibrium, thereby anchoring the local crossover between Recognition Science and FEP mechanics. The module explicitly notes that this 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.