F_eq_E_minus_TS
plain-language theorem explainer
The theorem proves that the Helmholtz free energy, defined as minus log of the partition function over beta, equals the expected energy under the Boltzmann distribution minus temperature times the entropy. Statistical mechanicians and variational inference researchers cite this when equating free-energy functionals to thermodynamic potentials. The proof is a direct algebraic expansion: it normalizes the probabilities, expands the entropy sum using log identities, and simplifies via ring and field tactics to recover the identity.
Claim. Let $E: I → ℝ$ assign real energies to a finite index set $I$ and let $β > 0$. Let $Z = ∑_i exp(−β E_i)$ be the partition function, $p_i = exp(−β E_i)/Z$ the Boltzmann probabilities, $⟨E⟩ = ∑_i p_i E_i$ the expected energy, and $S = −∑_i p_i log p_i$ the entropy. Then the Helmholtz free energy $F = −(1/β) log Z$ satisfies $F = ⟨E⟩ − (1/β) S$.
background
The module supplies concrete proofs for finite discrete systems, replacing abstract placeholders. The partition function is $Z = ∑_i exp(−β E_i)$, Boltzmann probability $p_i = exp(−β E_i)/Z$, expected energy $⟨E⟩ = ∑ p_i E_i$, and entropy $S = −∑ p_i log p_i$. Helmholtz free energy is defined as $F = −log Z / β$. This grounds the thermodynamic identity on a Fintype index set using only real analysis. Upstream results supply basic arithmetic facts such as one_mul and period definitions, though the core steps rely on properties of exp, log, and finite sums.
proof idea
Unfold the three definitions to expose the sums. Introduce Z as the partition sum and prove it positive and nonzero. Derive the log identity log(p_i) = −β E_i − log Z. Show probabilities sum to one. Expand the entropy sum to obtain β⟨E⟩ + log Z. Substitute into the target expression and finish with field_simp and ring.
why it matters
This is the fundamental discrete identity F = E − TS. It is invoked by the variational free energy theorem to show VFE at the Boltzmann distribution recovers the Helmholtz free energy, and it supplies the free_energy_identity field of the HelmholtzRealCert. In the Recognition Science setting it connects the recognition composition law and forcing chain (T5–T8) to thermodynamic potentials via the phi-ladder constants, closing the loop from abstract J-cost to measurable free energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.