Information Fepbridge From Jcost

The local bridge

The free-energy principle (FEP) is a framework in theoretical biology that describes how adaptive systems resist disorder by acting as if they minimize a quantity called variational free energy. In its common form, this quantity is a Kullback-Leibler (KL) divergence, a measure of how one probability distribution differs from a second, often written in terms of a ratio of probabilities. Recognition Science (RS) works with a different object, its ledger, a discrete record of recognition events, and the forced cost of maintaining that record. The cost function is J(x) = (x + x⁻¹) / 2 - 1, a formula that is proved in the framework's library to be the unique function satisfying five plain conditions. The question is how these two different starting points, one from biology and one from a theory of recognition, can be compared.

The FEP bridge module in the machine-checked library of formal theorems establishes a precise, local answer. The key move is to change coordinates. If you write the ratio x as exp(u), then the RS cost becomes J(exp(u)) = cosh(u) - 1. The FEP's KL divergence, in the same log-ratio coordinate, has a local quadratic proxy of u² / 2. The theorem-grade content is that these two expressions agree at equilibrium, which is the point u = 0, in their value, their first derivative, and their second derivative. The second derivative is the Fisher curvature, a measure of how sensitive the cost is to small changes. The library proves this contact is exact: jcost_log_exact states the cosh identity, and jcost_kl_same_second_order_at_equilibrium states the triple agreement. This is not an approximation; it is an exact local crossover between the two frameworks.

The module also sets up a scaffold for a deeper comparison. It defines the four state classes of the FEP's particular partition: external, sensory, active, and internal. It then defines a sparsity condition, HasMarkovBlanketSparsity, which says there is no direct coupling between internal and external states; all influence must pass through the sensory and active boundary states. This is the Markov blanket, the statistical boundary that separates an organism from its environment. The library proves that this condition is definitionally identical to a corresponding RS-side condition, HasLedgerBoundarySparsity, which has the same sparse-coupling shape for a recognition ledger boundary. The theorem markov_blanket_sparsity_iff_ledger_boundary_sparsity states this equivalence, and the structure FEPBridgeLocalCert packages all three results into a single certificate.

What this establishes in plain language is a point of contact, not a full unification. The local geometry of the RS cost function is exactly the same as the local geometry of the FEP's free energy at equilibrium, and the two frameworks describe the same kind of boundary sparsity. This is the theorem-grade part of the bridge. What it does not yet do is derive the Markov blanket or Bayesian filtering from the RS ledger dynamics. The hard follow-on, deriving HasLedgerBoundarySparsity from the cost dynamics for a concrete recognition field, remains open. The module names this remaining structure explicitly, so the bridge is a certified foundation for future work, not a completed crossing.

/-- In log coordinates, reciprocal J-cost is exactly `cosh u - 1`. -/
theorem jcost_log_exact (u : ℝ) :
    Jlog u = Real.cosh u - 1 :=
  Jlog_as_cosh u

/-- RS reciprocal cost and the KL quadratic have the same Fisher curvature
at equilibrium.  This is the exact local crossover with FEP-style free energy.
-/
theorem jcost_kl_same_second_order_at_equilibrium :
    Jlog 0 = klQuadratic 0 ∧
    deriv Jlog 0 = deriv klQuadratic 0 ∧
    deriv (deriv Jlog) 0 = deriv (deriv klQuadratic) 0 := by
  constructor
  · simp [Jlog_zero]
  constructor
  · simp
  · have hJ := hasDerivAt_deriv_Jlog_zero.deriv
    have hK := hasDerivAt_deriv_klQuadratic_zero.deriv
    rw [hJ, hK]

/-- The current bridge between FEP blankets and RS ledger boundaries is a
shape theorem: the two sparsity predicates are definitionally the same.

The hard follow-on is deriving `HasLedgerBoundarySparsity` from RCL/J-cost
dynamics for a concrete recognition field.
-/
theorem markov_blanket_sparsity_iff_ledger_boundary_sparsity (C : Coupling) :
    HasMarkovBlanketSparsity C ↔ HasLedgerBoundarySparsity C := by
  rfl

What this page does not claim

This does not claim that the free-energy principle and Recognition Science are equivalent frameworks. This does not claim that a Markov blanket has been derived from the ledger dynamics. This does not claim that the bridge applies beyond the local equilibrium point.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/FEPBridgeFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: