helmholtzF_well_defined
plain-language theorem explainer
The theorem confirms that the Helmholtz free energy for a finite discrete energy spectrum equals minus the natural logarithm of the partition function divided by the inverse temperature, for any nonzero inverse temperature. Thermodynamic derivations in the Recognition Science setting would cite this to fix the explicit form of F before deriving relations such as F = E - TS. The proof is immediate reflexivity on the definition of the free-energy function.
Claim. For a finite index set of states with energies $E_i$ and inverse temperature $β ≠ 0$, the Helmholtz free energy satisfies $F = - (ln Z)/β$, where the partition function is $Z = ∑_i exp(-β E_i)$.
background
This module supplies explicit real-valued theorems for the Helmholtz free energy on finite discrete systems, replacing the placeholder assertions in the abstract FreeEnergy module. The partition function is the sum over states of the Boltzmann factor exp(-β E_i). The Helmholtz free energy is introduced directly as the negative log of this sum scaled by 1/β. Upstream results include the general partition-function construction in BoltzmannDistribution and the J-cost bridge that links the same sum to Recognition Science cost functions.
proof idea
The proof is a one-line term that applies reflexivity directly to the definition of helmholtzF, which is written identically to the right-hand side.
why it matters
This equality anchors the explicit partition-function expression used throughout the thermodynamics development and supports sibling results such as F_eq_E_minus_TS. In the Recognition Science framework it grounds thermodynamic potentials in the finite-state partition function that arises from spectral emergence and J-cost structures. The module doc notes that the free energy is convex in β and that the Boltzmann distribution minimizes the free-energy functional via the Gibbs inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.