FEPStateClass
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not specify any coupling relations between the four classes.
- Does not derive the sparsity condition from the recognition composition law.
- Does not connect the partition to the phi-ladder or mass formulas.
- Does not address the Berry creation threshold or dream fraction.
formal statement (Lean)
94inductive FEPStateClass where
95 | external
96 | sensory
97 | active
98 | internal
99 deriving DecidableEq, Repr, BEq, Fintype
100
101/-- A sparse coupling relation between FEP state classes. -/