boltzmannEntropy
plain-language theorem explainer
boltzmannEntropy supplies the Shannon entropy of the discrete Boltzmann distribution over a finite index set as the negative sum of p log p. A researcher deriving the free-energy identity in statistical mechanics would cite it when connecting Helmholtz free energy to expected energy minus temperature times entropy. The definition is realized as a direct summation over the probabilities from boltzmannProb.
Claim. The entropy of the Boltzmann distribution is $S(E,β) := -∑_i p_i log p_i$, where $p_i = exp(-β E_i)/Z$ and $Z = ∑_j exp(-β E_j)$.
background
The HelmholtzReal module supplies concrete proofs for the finite discrete case of Helmholtz free energy. The partition function is defined as $Z(β) = ∑_i exp(-β E_i)$, the Boltzmann probabilities are $p_i = exp(-β E_i)/Z$, and the free energy is $F = -log Z / β$. The entropy concept builds on the defect-based definition in InitialCondition.entropy, which sets zero defect to minimum entropy. The module invokes the Gibbs inequality to establish that the Boltzmann distribution minimizes the functional $F[p] = ∑ p_i E_i - T H[p]$.
proof idea
This is a definition that directly transcribes the standard Shannon entropy formula. It applies the summation operator to the product of boltzmannProb E β i and its natural logarithm over the index set.
why it matters
boltzmannEntropy supplies the entropy term required for the identity F = E - T S proved in F_eq_E_minus_TS. It is invoked in vfe_at_boltzmann_eq_helmholtzF to equate variational free energy at the Boltzmann reference to the Helmholtz free energy. This anchors the thermodynamic relations inside the Recognition framework's discrete setting and supports the free-energy minimization principle stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.