FEPBridgeLocalCert
plain-language theorem explainer
FEPBridgeLocalCert packages three local matching conditions between Recognition Science J-cost and Friston FEP: exact equality of the log-domain cost to cosh u minus one, second-order contact of derivatives at equilibrium between Jlog and the KL quadratic, and definitional equivalence of Markov-blanket sparsity with ledger-boundary sparsity. Researchers comparing variational inference to recognition dynamics would cite this certificate when anchoring RS to active-inference models. The definition directly assembles three sibling lemmas that fill
Claim. Let $J(u) := J(e^u)$ where $J$ is the Recognition cost. The structure asserts three properties: $J(u) = 2^{-1}(e^u + e^{-u}) - 1$ for all real $u$; the value, first derivative, and second derivative of $J$ and the KL quadratic agree at $u=0$; and for every coupling relation $C$, the Markov-blanket sparsity predicate on $C$ holds if and only if the ledger-boundary sparsity predicate on $C$ holds.
background
The module anchors comparison of Recognition Science with Friston-style free-energy-principle mechanics. Recognition Science uses the reciprocal cost $J(x) = (x + x^{-1})/2 - 1$. In log-ratio coordinates $x = e^u$ this becomes $J(e^u) = cosh u - 1$, so the local quadratic contact with Fisher/KL geometry is exact at value, first derivative, and second derivative at equilibrium. The module doc states that this marks the theorem-grade part of the bridge and names the remaining structure.
proof idea
The structure is defined by packaging three sibling lemmas: jcost_log_exact supplies the exact_log_cost field, jcost_kl_same_second_order_at_equilibrium supplies the fisher_contact field, and markov_blanket_sparsity_iff_ledger_boundary_sparsity supplies the blanket_boundary_shape field. No additional tactics or reductions are applied.
why it matters
FEPBridgeLocalCert supplies the local FEP/RS bridge certificate instantiated in fepBridgeLocalCert and shown inhabited by fep_bridge_local_cert_holds. It marks the theorem-grade part of the bridge, citing the exact local quadratic contact with KL geometry. The open question it touches is derivation of HasLedgerBoundarySparsity from the Recognition Composition Law rather than assuming the partition as a shape theorem. This aligns with J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.