IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL
This module constructs variational free energy from the Recognition Composition Law on finite discrete probability distributions. It bridges Recognition Science J-cost to Friston-style FEP mechanics and supplies the statistical layer for downstream filtering results. Researchers in active inference or statistical mechanics cite it for the VFE-Helmholtz equivalence at equilibrium. The module proceeds via definitions of distributions and Boltzmann states followed by non-negativity and minimization lemmas.
claimLet $ι$ be finite. A probability distribution is a map $q:ι→ℝ_{>0}$ with $∑_{i∈ι} q_i=1$. The variational free energy $VFE(q)$ is obtained from the J-cost via the Recognition Composition Law and satisfies $VFE(q)≥F$ with equality at the Boltzmann distribution, where $F$ denotes the Helmholtz free energy.
background
The module operates over finite discrete spaces and imports the J-cost definition from the Cost module together with the FEPBridgeFromJCost module, whose doc-comment states it is 'the first Lean anchor for comparing Recognition Science with Friston-style free-energy-principle (FEP) mechanics' using KL and variational free energy while RS uses reciprocal cost. It further imports HelmholtzReal, which supplies real proofs for Helmholtz free energy minimization on finite sets in place of earlier trivial placeholders.
proof idea
This is a definition module, no proofs. It introduces ProbDist as positive unit-sum functions, defines VFE and boltzmannDist, then records the lemmas kl_nonneg, vfe_at_boltzmann_eq_helmholtzF, boltzmann_minimizes_vfe together with the certificate VFECert and the witness vfeCert_holds.
why it matters in Recognition Science
This module supplies the variational free energy foundation required by the downstream BayesianFilteringFromVFE, whose doc-comment states 'a Bayesian update is the one-step VFE minimizer'. It realizes the statistical bridge from the Recognition Composition Law to thermodynamic free energies, enabling the discrete filtering surface in the Recognition framework.
scope and limits
- Does not address continuous or infinite state spaces.
- Does not derive dynamical equations for free-energy flow.
- Does not connect to the phi-ladder or RS-native constants.
- Does not treat approximation schemes or numerical evaluation.