fep_bridge_local_cert_holds
plain-language theorem explainer
The theorem asserts existence of a compact certificate establishing that Recognition Science's J-cost in logarithmic coordinates equals cosh u minus one, matches the KL quadratic in value and first two derivatives at equilibrium, and equates Markov blanket sparsity with ledger boundary sparsity for couplings. Information theorists comparing RS to Friston's free-energy principle would cite it as the initial theorem-grade local bridge. The proof is a one-line term wrapper that directly instantiates the certificate from prior exact-matching lemmas
Claim. There exists a certificate such that the reciprocal cost satisfies $J(e^u) = e^u + e^{-u} - 2)/2 = cosh u - 1$ for all real $u$, the value, first derivative, and second derivative of this cost agree with those of the KL quadratic approximation at $u=0$, and for every coupling the Markov blanket sparsity condition is equivalent to the ledger boundary sparsity condition.
background
The module supplies the first Lean anchor for comparing Recognition Science with Friston-style free-energy-principle mechanics. Recognition Science employs the reciprocal cost $J(x) = (x + x^{-1})/2 - 1$, which in log-ratio coordinates $x = e^u$ becomes $J(e^u) = cosh u - 1$. The KL quadratic is the second-order Taylor expansion of the Kullback-Leibler divergence around equilibrium. The certificate structure records three facts: exact equality of the log-cost to cosh minus one, agreement of value plus first and second derivatives with the KL quadratic at zero, and equivalence of Markov blanket sparsity to ledger boundary sparsity for any coupling. The upstream definition assembles these three facts from exact log-cost equivalence, second-order Fisher contact, and the blanket-boundary equivalence lemma.
proof idea
The proof is a one-line term wrapper that applies the definition of the local FEP/RS bridge certificate. That definition in turn packages the exact log-cost lemma, the second-order matching lemma for J-cost and KL quadratic, and the Markov-blanket-to-ledger-boundary equivalence.
why it matters
This supplies the first Lean-certified local contact between Recognition Science's J-cost and the variational free energy of the free-energy principle. It fills the theorem-grade part of the FEP bridge described in the module documentation, leaving open the derivation of Markov blankets and Bayesian filtering directly from the Recognition Composition Law. It confirms the cosh form that follows from J-uniqueness in the forcing chain and marks the boundary between proved local geometry and the remaining global structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.