Information Fepbridge From Jcost Fepbridge Local Cert

The local bridge certificate

The free energy principle (FEP) in neuroscience and theoretical biology describes how a system like a brain or an organism maintains its internal states by minimizing a quantity called variational free energy, a measure of surprise or prediction error. Recognition Science (RS) starts from a different object: a forced cost, a number that measures the price of a recognition event, which its framework proves must take the form J(x) = (x + 1/x)/2 - 1. The declaration FEPBridgeLocalCert is a compact, machine-checked record of the exact points where these two descriptions touch.

The certificate contains three statements. First, in logarithmic coordinates, the RS cost equals cosh(u) - 1, a standard hyperbolic function. Second, at the equilibrium point u = 0, this cost and the quadratic approximation used in FEP share the same value, the same first derivative, and the same second derivative. This second derivative is the Fisher curvature, a measure of how sharply the cost rises as the system moves away from equilibrium; the certificate proves the two geometries curve identically at that single point. Third, the certificate records that the sparsity condition defining a Markov blanket, the boundary that separates a system's internal states from its external environment, is formally identical to the sparsity condition defining a recognition-ledger boundary in RS.

These three facts are proved in the framework's machine-checked library of formal theorems, meaning the certificate is not a conjecture but a verified statement. Its value is that it names precisely where a future derivation could connect FEP's variational free energy to RS's forced cost: at the level of local curvature, the two agree. The certificate is deliberately local, a point of contact rather than a full equivalence.

What the certificate does not claim is as important as what it proves. It does not derive Markov blankets or Bayesian filtering from RS dynamics; it only shows that a certain sparsity shape, the absence of direct internal-external coupling, is the same in both frameworks. The hard problem of deriving that boundary condition from the recognition cost itself remains open. The certificate is a map of a single meeting point, not a claim that the two theories are the same.

/-- 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 or Bayesian filtering from RS dynamics. The certificate does not prove that FEP and RS are the same theory, only that they share a local curvature and a boundary shape. The certificate does not claim the recognition-ledger boundary condition is forced by the cost; that derivation remains open.

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: