freeEnergy
plain-language theorem explainer
The declaration defines the Helmholtz free energy of a discrete system as F = -k_B T ln Z, where Z is the partition function summed over ledger configurations weighted by J-cost. Statistical mechanicians working inside the Recognition Science framework cite this expression to recover thermodynamic potentials directly from the ledger structure. The definition is a direct one-line algebraic wrapper around the partition function and the Boltzmann constant.
Claim. The Helmholtz free energy of a discrete system at positive temperature $T$ is given by $F = -k_B T$ ln $Z$, where $Z$ is the partition function of the system.
background
DiscreteSystem is a finite structure consisting of numLevels energy levels, each carrying an energy value and a positive degeneracy. The partition function Z is formed as the sum over these levels of degeneracy times exp(-beta E_i), with beta = 1/(k_B T). In the Recognition Science setting this sum arises as a ledger sum weighted by J-cost rather than an arbitrary postulate.
proof idea
One-line definition that directly applies the partitionFunction to the supplied system and temperature, then multiplies by -k_B T.
why it matters
This definition supplies the free energy expression used by the downstream free_energy_identity theorem to prove F = averageEnergy - T S. It realizes the core claim of THERMO-002 that the partition function encodes all thermodynamic information once Z is obtained from the RS ledger. The construction sits inside the thermodynamics domain and inherits k_B from the Landauer bound established in ComputationLimitsStructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.