FEPStateClass
plain-language theorem explainer
FEPStateClass enumerates the four partitions used in the free energy principle comparison to Recognition Science. Researchers establishing the sparse coupling structure between internal and external states cite this definition when setting up the boundary conditions. The construction is a direct inductive enumeration that automatically derives decidable equality and finite type instances.
Claim. The inductive type consisting of four elements: external, sensory, active, and internal states.
background
This module supplies the first Lean anchor comparing Recognition Science J-cost to Friston-style free-energy mechanics. J-cost is given by J(x) = (x + x^{-1})/2 - 1, which equals cosh(u) - 1 in log-ratio coordinates x = exp(u). The module states that the local quadratic contact with Fisher/KL geometry is exact at equilibrium in value, first derivative, and second derivative.
proof idea
The declaration is an inductive definition that enumerates the four state classes by cases. It derives the DecidableEq, Repr, BEq, and Fintype instances via the deriving clause.
why it matters
This definition supplies the state partition required by the downstream Coupling relation and the sparsity predicates HasMarkovBlanketSparsity and HasLedgerBoundarySparsity. It marks the initial theorem-grade anchor in the FEP bridge from J-cost, as noted in the module documentation. Future work must still derive the Markov blanket sparsity from the recognition composition law rather than assume the partition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.