HasMarkovBlanketSparsity
plain-language theorem explainer
HasMarkovBlanketSparsity defines the predicate that a coupling relation C between FEP state classes has no direct internal-to-external link and no direct external-to-internal link. Researchers bridging variational free-energy mechanics to Recognition Science ledger dynamics cite this predicate to mark the local sparsity condition. The definition is introduced directly as the conjunction of two negated coupling propositions with no auxiliary lemmas.
Claim. Let $C$ be a relation on FEP state classes. The predicate holds precisely when $C$ does not relate the internal class to the external class and does not relate the external class to the internal class.
background
The module supplies the first Lean anchor for comparing Recognition Science reciprocal cost with Friston-style free-energy mechanics. The cost is $J(x) = (x + x^{-1})/2 - 1$, which becomes $J(e^u) = cosh(u) - 1$ in log-ratio coordinates and matches the KL quadratic together with its first two derivatives at equilibrium. The coupling is defined as an abbrev $FEPStateClass → FEPStateClass → Prop$ that encodes sparse relations required to route through boundary states. Upstream results include ledger factorization structures and phi-forcing derivations that calibrate the cost function.
proof idea
The declaration is a direct definition that expands to the conjunction of the two negated coupling statements on the internal and external classes. No tactics or lemmas are invoked; the body simply records the sparsity shape.
why it matters
The predicate supplies the FEP-side sparsity condition shown to be definitionally identical to ledger-boundary sparsity by the companion theorem markov_blanket_sparsity_iff_ledger_boundary_sparsity. It completes the theorem-grade portion of the FEP bridge recorded in FEPBridgeLocalCert, which also certifies the exact quadratic contact between J and the KL quadratic. The remaining open task is derivation of the sparsity predicate from the recognition composition law and J-cost dynamics rather than by assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.