fepBridgeLocalCert
The definition constructs the local FEP/RS bridge certificate by packaging the exact match of reciprocal J-cost to cosh u minus 1 in log coordinates, the second-order agreement with the KL quadratic at equilibrium, and the equivalence of Markov blanket sparsity with ledger boundary sparsity. Researchers comparing Recognition Science to Friston's free energy principle would cite this as the precise local crossover point. It is a direct construction that invokes three upstream theorems to fill the fields of the FEPBridgeLocalCert structure.
claimThe local bridge certificate is the structure instance satisfying $J(u) = (e^u + e^{-u})/2 - 1$ for all real $u$, with this function and the KL quadratic approximation agreeing in value, first derivative, and second derivative at the equilibrium point $u=0$, together with the equivalence that Markov blanket sparsity holds for a coupling $C$ if and only if ledger boundary sparsity holds for the same $C$.
background
In Recognition Science the reciprocal cost is $J(x) = (x + x^{-1})/2 - 1$. In logarithmic coordinates $u = log x$ this becomes $J(u) = cosh u - 1$. The module establishes the local contact between this cost and the variational free energy of the free-energy principle, which is approximated by the KL quadratic near equilibrium. The FEPBridgeLocalCert structure collects three pieces: the exact logarithmic identity, the matching Fisher information (second derivative) at equilibrium, and the definitional equivalence between Markov blanket sparsity and ledger boundary sparsity. Upstream, the theorem establishing the cosh identity reduces directly to the definition of the log cost, while the equilibrium theorem establishes the three equalities at zero by direct computation of derivatives. This local certificate marks the theorem-grade part of the bridge without yet deriving the full Markov blanket structure from the Recognition Composition Law.
proof idea
The definition is a direct constructor that supplies the three fields of the FEPBridgeLocalCert structure. It uses the theorem proving the exact logarithmic identity to witness the cost field, the theorem proving second-order agreement at equilibrium to witness the Fisher contact field, and the theorem proving the sparsity equivalence to witness the blanket-boundary field. No additional tactics are required beyond the constructor application.
why it matters in Recognition Science
This definition supplies the witness for the theorem asserting that the FEPBridgeLocalCert structure is inhabited. It therefore closes the local bridge between Recognition Science reciprocal cost and FEP variational free energy at the level of value, first and second derivatives. The result sits at the interface of the J-cost formalism and information geometry, confirming the exact quadratic contact at equilibrium that is required for any deeper comparison of the two frameworks. The remaining open question is the derivation of ledger boundary sparsity from Recognition Composition Law dynamics for a concrete recognition field.
scope and limits
- Does not derive Markov blankets or Bayesian filtering from the Recognition Composition Law.
- Does not establish a global equivalence between FEP mechanics and Recognition Science.
- Does not compute explicit numerical values for the Fisher information or higher-order terms.
- Does not address non-equilibrium dynamics or finite-size corrections.
Lean usage
theorem fep_bridge_local_cert_holds : Nonempty FEPBridgeLocalCert := ⟨fepBridgeLocalCert⟩formal statement (Lean)
139noncomputable def fepBridgeLocalCert : FEPBridgeLocalCert where
140 exact_log_cost := jcost_log_exact
proof body
Definition body.
141 fisher_contact := jcost_kl_same_second_order_at_equilibrium
142 blanket_boundary_shape := markov_blanket_sparsity_iff_ledger_boundary_sparsity
143