Coupling
plain-language theorem explainer
The sparse coupling relation between FEP state classes encodes the Markov-blanket sparsity condition in the bridge from J-cost geometry to Friston's free-energy principle. Neuroscientists and physicists comparing active inference models to Recognition Science cite this interface when enforcing boundary routing. It is introduced as a direct abbreviation of the binary predicate on the four-state partition.
Claim. Let $F$ be the inductive partition of states into external, sensory, active and internal classes. The sparse coupling relation is the predicate $F → F → Prop$ that holds only when two classes may interact directly, with the requirement that all internal-external interaction routes through the sensory-active boundary.
background
The module FEPBridgeFromJCost supplies the first Lean anchor for comparing Recognition Science with Friston-style free-energy-principle mechanics. Recognition Science uses the reciprocal cost $J(x) = (x + x^{-1})/2 - 1$, which equals cosh u - 1 in log-ratio coordinates. The module states that the local quadratic contact with the Fisher/KL geometry is exact at equilibrium up to second order, while noting that Markov blankets and Bayesian filtering are not yet derived from the Recognition Composition Law.
proof idea
The declaration is a one-line abbreviation that directly instantiates the binary predicate type on the inductive FEPStateClass.
why it matters
This definition supplies the sparsity interface referenced by thirty-four downstream declarations, including alignment_quality, cooper_pair_binding_exceeds_thermal, LabScalePrediction, J_log_error_bound, bridge_chain_complete and equilibrium_is_coherent. The module documentation states that the result is deliberately local and marks the theorem-grade part of the bridge while naming the remaining structure. It connects to the J-uniqueness step and the Recognition Composition Law in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.