Information Fepbridge From Jcost Has Deriv At Deriv Kl Quadratic Zero

The local contact

In information theory, the Kullback-Leibler (KL) divergence measures how one probability distribution differs from a reference distribution. Its local, quadratic approximation in a single log-ratio coordinate u is u²/2. This is a standard object: the Fisher information metric, the curvature of statistical distance.

Recognition Science (RS) begins from a different object, a ledger (a discrete record of recognition events) and a forced cost function J(x) = (x + x⁻¹)/2 - 1. In log coordinates x = exp u, this cost becomes exactly cosh u - 1, a fact proved in the framework's machine-checked library of formal theorems. The question is how these two measures of deviation relate.

The framework's library proves a local contact: at the equilibrium point u = 0, the RS cost and the KL quadratic have the same value (zero), the same first derivative (zero), and the same second derivative (one). The declaration hasDerivAt_deriv_klQuadratic_zero is the precise statement that the derivative of the KL quadratic has derivative 1 at 0, which is the curvature match. This is the exact local crossover where RS cost and FEP-style free energy agree to second order.

This is a theorem about a local quadratic proxy, not a derivation of the full free-energy principle. The framework explicitly does not yet derive Markov blankets or Bayesian filtering from its ledger dynamics. The blanket sparsity condition is only shown to have the same shape as a ledger boundary condition, a definitional equivalence, not a physical derivation. The hard follow-on, deriving the boundary condition from the cost dynamics, 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 second derivative of the KL quadratic at equilibrium is `1`. -/
theorem hasDerivAt_deriv_klQuadratic_zero :
    HasDerivAt (deriv klQuadratic) 1 0 := by
  have h_eq : deriv klQuadratic = fun u : ℝ => u := by
    funext u
    exact (hasDerivAt_klQuadratic u).deriv
  rw [h_eq]
  simpa using (hasDerivAt_id 0)

/-- 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 derive Markov blankets or Bayesian filtering from the recognition ledger. The blanket sparsity equivalence is a shape theorem, not a physical derivation. The local contact does not establish a global equivalence between RS cost and free energy.

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: