Information Fepbridge From Jcost Jcost Log Exact

The exact log-coordinate identity

In the Recognition Science framework, the cost of a recognition event is forced by five plain conditions to take the form J(x) = (x + x⁻¹)/2 − 1. The declaration jcost_log_exact establishes what this cost looks like when measured on a logarithmic scale. If you set x = e^u, the cost becomes exactly J(e^u) = cosh(u) − 1. This is a proved theorem in the framework's machine-checked library of formal theorems: for every real number u, the log-coordinate cost equals the hyperbolic cosine minus one.

The identity matters because cosh(u) − 1 is the standard local approximation to Kullback-Leibler divergence, the quantity used in Friston-style free-energy mechanics. The theorem shows that the framework's cost function and the KL quadratic u²/2 agree at equilibrium in value, first derivative, and second derivative. This is the exact local crossover between Recognition Science and free-energy approaches: near the equilibrium point, the two descriptions of cost are indistinguishable to second order. The declaration also proves that the Markov-blanket sparsity condition used in free-energy mechanics is definitionally the same shape as the framework's ledger-boundary condition.

What the theorem does not claim is just as important as what it proves. It does not derive Markov blankets, Bayesian filtering, or any full free-energy principle from the framework's dynamics. The bridge is deliberately local: it establishes a precise contact point between two cost geometries, not an equivalence of entire theories. The hard follow-on, deriving the ledger-boundary condition from the recognition-cost dynamics for a concrete field, remains open.

/-- 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

The theorem does not derive Markov blankets or Bayesian filtering from the framework's dynamics. The identity does not equate Recognition Science with the full free-energy principle. The local contact does not claim agreement between the two cost functions away from equilibrium.

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: