boltzmannDist
plain-language theorem explainer
The Boltzmann distribution on a finite index set ι is the probability measure whose masses are proportional to exp(−β E_i) for a given energy function E and inverse temperature β. Researchers working on discrete variational inference or free-energy minimization in the Recognition Science setting cite this construction as the canonical reference measure. The definition is a direct structure constructor that packages the probability function, positivity proof, and normalization from the HelmholtzReal module.
Claim. Let ι be a finite type. For an energy map E : ι → ℝ and parameter β ∈ ℝ the Boltzmann distribution is the element p ∈ ProbDist ι whose probability masses satisfy p(i) = exp(−β E(i)) / Z with Z = ∑_j exp(−β E(j)), together with the proofs that each mass is positive and the masses sum to one.
background
In VariationalFreeEnergyFromRCL the variational free energy is defined on the simplex of probability distributions. ProbDist ι is the structure consisting of a function prob : ι → ℝ together with proofs prob_pos : ∀ i, 0 < prob i and prob_sum : ∑ i, prob i = 1. The module imports the Boltzmann probability construction from Thermodynamics.HelmholtzReal, which supplies boltzmannProb E β i together with its positivity and summation-to-one properties. This construction sits inside the broader Recognition Science program that derives statistical mechanics from the Recognition Composition Law (RCL) and the J-cost functional. The local setting is a finite recognition partition on which the Friston VFE F[q ; E, β] = ∑ q_i E_i − (1/β) H[q] is to be minimized.
proof idea
The definition is a one-line wrapper that assembles the three fields of the ProbDist structure by direct appeal to boltzmannProb, boltzmannProb_pos and boltzmannProb_sum_one imported from HelmholtzReal.
why it matters
This definition supplies the reference measure that is shown in the downstream theorems boltzmann_minimizes_vfe and vfe_at_boltzmann_eq_helmholtzF to achieve the global minimum of the variational free energy and to recover the Helmholtz free energy. It therefore closes the loop between the Recognition Composition Law and the canonical form of free energy in statistical mechanics, confirming that the Boltzmann distribution is the unique minimizer on any finite partition. The construction is used inside the VFECert certificate that packages both the equality to HelmholtzF and the minimization property.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.