Information Fepbridge From Jcost Markov Blanket Sparsity Iff Ledger Boundary Spa

The shape equivalence

A Markov blanket is the set of states that separates a system's internal states from its external environment: sensory and active states form a boundary through which all influence must pass. In the free-energy principle, this blanket is a foundational assumption about how any self-organizing system is partitioned. The Recognition Science framework, which starts from a ledger (a discrete record of recognition events), has its own boundary concept with the same sparse-coupling shape: no direct internal-external coupling in either direction.

The declaration markov_blanket_sparsity_iff_ledger_boundary_sparsity proves that these two sparsity predicates are definitionally the same. For any coupling relation between the four state classes (external, sensory, active, internal), having a Markov blanket is equivalent to having a ledger boundary. The proof is by reflexivity: the two definitions are literally identical in the framework's formal language. This is a shape theorem, not a derivation. The framework has not yet shown that recognition dynamics force a Markov blanket to exist; it has shown that if you write down either boundary condition, you have written down the other.

The same module also establishes a local contact between the framework's reciprocal cost and the KL divergence used in free-energy mechanics. In log-ratio coordinates, the reciprocal cost J(x) = (x + x⁻¹)/2 − 1 becomes exactly cosh u − 1, and at equilibrium this matches the quadratic KL proxy u²/2 in value, first derivative, and second derivative. This is the exact local crossover: the two frameworks agree on curvature at the equilibrium point, which is the Fisher information geometry.

What this does not claim is the hard part. The theorem does not derive Markov blankets or Bayesian filtering from recognition dynamics. It does not show that a recognition field will spontaneously form a boundary. The docstring names this as the remaining structure: future work must derive the ledger boundary condition from the ledger forcing dynamics for a concrete recognition field. The current result is a certificate that the two vocabularies meet at the same shape, not a proof that either vocabulary produces that shape on its own.

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

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

What this page does not claim

The theorem does not derive Markov blankets or Bayesian filtering from recognition dynamics. The theorem does not show that a recognition field will spontaneously form a boundary.

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: