Information Fepbridge From Jcost Fep Bridge Local Cert Holds

The local bridge certificate

The free-energy principle (FEP) is a framework in theoretical biology that describes how adaptive systems resist disorder by minimizing a quantity called variational free energy. Recognition Science (RS) is a separate framework built from a different starting point: a discrete record of events called a ledger, where each recognition event carries a forced cost. The declaration fep_bridge_local_cert_holds is a machine-checked certificate that records where these two frameworks make contact, and it is deliberately limited in scope.

The certificate's first component is an exact identity. In log-ratio coordinates, where a state variable x is written as exp(u), the RS cost function J(x) = (x + 1/x)/2 - 1 becomes J(exp u) = cosh u - 1. This is not an approximation; the machine-checked theorem proves the equality for every real number u. The second component is a contact at equilibrium. At u = 0, which corresponds to x = 1, both the RS cost and the FEP's local quadratic proxy for KL divergence (the function u²/2) have the same value, the same first derivative, and the same second derivative. This means the two frameworks share the same local curvature, what a physicist would call the same Fisher information metric, at the point of equilibrium.

The third component concerns the shape of boundaries. FEP describes systems as partitioned into internal, external, sensory, and active states, with a Markov blanket separating internal from external. The certificate proves that the sparsity condition defining a Markov blanket is definitionally identical to the sparsity condition defining an RS ledger boundary. Both require that there be no direct coupling between internal and external states; all influence must pass through the sensory and active states in between. This is a shape theorem: the two predicates are the same by definition.

In Recognition Science, this certificate establishes the theorem-grade part of the bridge to FEP mechanics. It proves that the local geometry of RS cost matches the local geometry of FEP free energy, and that the boundary structure has the same shape. It does not claim that RS derives Markov blankets from its ledger dynamics, nor that it derives Bayesian filtering, nor that the FEP's partition of states into four classes follows from RS first principles. Those remain open targets. The certificate is a precise record of what is currently known, and a clear map of what is not.

/-- 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 certificate does not derive Markov blankets from RS first principles. This certificate does not derive Bayesian filtering from RS cost. This certificate does not claim the FEP partition into four state classes follows from RS dynamics.

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: