Information Fepbridge From Jcost Has Deriv At Kl Quadratic

The local crossover

The KL divergence is a standard information-theoretic measure of how one probability distribution differs from a second. In a single log-ratio coordinate, its local quadratic approximation is simply u²/2. The declaration hasDerivAt_klQuadratic establishes that this quadratic function has a derivative at every real point u, and that the derivative equals u. This is a basic calculus fact, but the framework's library proves it formally as part of a bridge to Friston-style free-energy-principle mechanics.

In Recognition Science, the central object is the cost function J(x) = (x + x⁻¹)/2 − 1, which measures the price of a recognition event. In log-ratio coordinates x = exp u, this becomes exactly cosh u − 1. The theorem jcost_log_exact proves this identity. The significance is that cosh u − 1 and u²/2 agree to second order at u = 0: both are zero, both have zero first derivative, and both have second derivative equal to 1. The theorem jcost_kl_same_second_order_at_equilibrium packages this agreement as a single formal statement.

This local contact means that near equilibrium, the framework's cost function and the KL quadratic are indistinguishable up to second order. The framework's library proves this as a theorem-grade result, not a conjecture. It is the first Lean anchor for comparing Recognition Science with FEP mechanics, which uses KL or variational free energy. The practical payoff is that any calculation relying only on local curvature near equilibrium can use the simpler quadratic form without changing the answer.

The declaration does not claim more than this local agreement. It does not derive Markov blankets or Bayesian filtering from the recognition-cost law. The library defines a Markov-blanket sparsity condition and shows it is definitionally identical to a ledger-boundary sparsity condition, but deriving the latter from cost dynamics for a concrete field remains open. The bridge is deliberately local: it marks the theorem-grade part and names the remaining structure as future work.

/-- The KL quadratic has zero first derivative at equilibrium. -/
theorem hasDerivAt_klQuadratic (u : ℝ) :
    HasDerivAt klQuadratic u u := by
  unfold klQuadratic
  have hsq : HasDerivAt (fun v : ℝ => v ^ 2) (2 * u) u := by
    simpa using (hasDerivAt_pow 2 u)
  have h := hsq.div_const 2
  convert h using 1
  ring

/-- 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 derive Markov blankets or Bayesian filtering from the recognition-cost law. This does not claim the cost function equals the KL divergence globally, only to second order at equilibrium. This does not establish that the sparsity shape theorem holds for any concrete physical system.

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: