helmholtzF
plain-language theorem explainer
The definition supplies the Helmholtz free energy for a discrete energy spectrum as the negative logarithm of the partition function divided by inverse temperature. Variational free energy derivations and discrete thermodynamics cite this expression when equating the VFE minimum to the thermodynamic potential. It is realized by a direct one-line abbreviation that invokes the partition function sum and the real logarithm.
Claim. The Helmholtz free energy for a finite set of states with energies $E_i$ at inverse temperature $β$ is $F = - (1/β) log Z$, where the partition function is the sum $Z = ∑_i exp(-β E_i)$.
background
The HelmholtzReal module supplies real-number proofs for thermodynamic relations previously asserted as trivial placeholders in FreeEnergy. The partition function is defined as the sum over states of the Boltzmann factor exp(-β E_i). The Helmholtz free energy is obtained by taking the negative logarithm of this sum and scaling by the inverse temperature.
proof idea
The definition is a direct one-line abbreviation. It applies the partition function definition to form the sum of exponentials, then composes with the real logarithm and division by beta.
why it matters
This definition is the central object in the discrete thermodynamics layer. It is invoked by the variational free energy certification theorems that show the Boltzmann distribution minimizes the VFE and that the VFE at the Boltzmann point equals the Helmholtz free energy. It also supports the identity relating free energy to expected energy minus temperature times entropy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.