HasLedgerBoundarySparsity
plain-language theorem explainer
The definition introduces the recognition-ledger boundary sparsity condition: a coupling relation C between FEP state classes has no direct internal-to-external link and no external-to-internal link. Researchers comparing free-energy principle models to J-cost recognition dynamics cite it as the RS counterpart to Markov blanket sparsity. The predicate is introduced by direct conjunction of two negated coupling statements with no lemmas required.
Claim. Let $C$ be a coupling relation on FEP state classes. Ledger boundary sparsity holds when there is no direct coupling from the internal class to the external class and none from the external class to the internal class: $¬C( internal , external ) ∧ ¬C( external , internal )$.
background
The module supplies the first Lean anchor for comparing Friston-style free-energy principle mechanics, built on KL divergence and variational free energy, with Recognition Science, which uses the reciprocal cost $J(x) = (x + x^{-1})/2 - 1$. In log-ratio coordinates this is $J(e^u) = cosh u - 1$, producing exact second-order contact with Fisher geometry at equilibrium. The module is deliberately local and does not yet derive Markov blankets from RCL dynamics.
proof idea
The declaration is a direct definition of the sparsity predicate. It encodes the condition as the conjunction of two negated coupling statements under the supplied relation C. No upstream lemmas are invoked; the body is the propositional definition itself.
why it matters
This predicate supplies the RS-side sparsity object that feeds the local certificate structure and the definitional equivalence theorem showing Markov blanket sparsity is identical to ledger boundary sparsity. It marks the theorem-grade part of the FEP bridge while flagging the remaining task of deriving the condition from RCL and J-cost dynamics on a concrete recognition field. The module context connects to the broader forcing chain through the cost functions imported from observer forcing and multiplicative recognizers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.