IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL
This module derives variational free energy from the Recognition Composition Law by introducing probability distributions on finite sets and linking them to J-cost. It establishes that the Boltzmann distribution minimizes VFE and equates the minimum to Helmholtz free energy. Researchers bridging Recognition Science to Friston's free-energy principle cite it for the statistical mechanics foundation. The module consists of definitions plus short lemmas on non-negativity and minimization.
claimLet $ι$ be finite. A probability distribution is a map $p:ι→ℝ_{>0}$ with $∑p=1$. Variational free energy VFE is obtained from the J-cost bridge; the Boltzmann distribution $p∝exp(-E)$ minimizes it, with the minimum equal to the Helmholtz free energy.
background
The module sits in the statistics domain and imports Cost, FEPBridgeFromJCost, and HelmholtzReal. FEPBridgeFromJCost states: 'This module is the first Lean anchor for comparing Recognition Science with Friston-style free-energy-principle (FEP) mechanics. The result is deliberately local. FEP uses KL / variational free energy, while RS uses the reciprocal cost.' HelmholtzReal supplies real proofs for Helmholtz free energy on finite sets. The DOC_COMMENT defines a probability distribution on $ι$ as a positive function summing to 1.
proof idea
This is a definition module, no proofs. It introduces ProbDist, VFE, boltzmannDist together with the supporting lemmas kl_nonneg, vfe_at_boltzmann_eq_helmholtzF, boltzmann_minimizes_vfe and the certificate VFECert.
why it matters in Recognition Science
The module feeds BayesianFilteringFromVFE, whose doc-comment states: 'Discrete filtering surface: a Bayesian update is the one-step VFE minimizer.' It supplies the RCL-derived statistical layer required for that downstream result and closes the local RS-to-FEP bridge begun in FEPBridgeFromJCost.
scope and limits
- Does not treat continuous or infinite state spaces.
- Does not derive dynamical equations of the free-energy principle.
- Does not compute explicit numerical VFE values for concrete models.
- Does not address quantum or field-theoretic extensions.