freeEnergy
plain-language theorem explainer
Free energy is defined as F = -T ln Z for a System of energy levels at inverse temperature beta. Researchers deriving statistical mechanics from J-cost would cite it to obtain the Helmholtz potential from the partition function. The definition is a direct one-line expression that scales the logarithm of the module's partitionFunction by the temperature factor.
Claim. The Helmholtz free energy of a system is $F = -T(b) · ln Z(b)$, where $Z(b)$ is the partition function over the system's energy levels and $T(b)$ is the temperature at inverse temperature $b$.
background
In the BoltzmannDistribution module a System is a nonempty list of EnergyLevel structures. The partition function sums Boltzmann factors exp(-beta E_i) over those levels, with beta acting as the Lagrange multiplier for the fixed J-cost constraint. The module derives the Boltzmann distribution P_i proportional to exp(-beta E_i) from cost-weighted state selection under ledger balance, as stated in the module doc-comment.
proof idea
One-line definition that applies the standard Helmholtz formula using the partitionFunction and temperature scaling from the module.
why it matters
This definition feeds the free_energy_identity theorem that proves F equals averageEnergy minus temperature times entropy. It supplies the thermodynamic potential needed for the paper's claim that statistical mechanics follows from Recognition Science's J-cost functional, linking directly to the T5 J-uniqueness and T6 phi fixed-point steps in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.