HelmholtzRealCert
plain-language theorem explainer
HelmholtzRealCert bundles positivity of the partition function, normalization of the Boltzmann probabilities, and the identity F = ⟨E⟩ - T S for finite discrete energy spectra. A statistical mechanician working with exact finite-state models would cite it to ground the standard thermodynamic relations in explicit sums. The structure is assembled by direct field assignment from the three supporting theorems partitionFunction_pos, boltzmannProb_sum_one, and F_eq_E_minus_TS.
Claim. Let $Z = Z(E,β) = ∑_i exp(-β E_i)$ be the partition function over a finite nonempty index set. Then $Z > 0$, the probabilities $p_i = exp(-β E_i)/Z$ satisfy ∑ p_i = 1, and for β > 0 the Helmholtz free energy $F = -β^{-1} log Z$ obeys $F = ⟨E⟩ - β^{-1} S$ where ⟨E⟩ = ∑ p_i E_i and $S = -∑ p_i log p_i$.
background
The module works exclusively with finite Fintype index sets ι and real-valued energies E : ι → ℝ. The partition function is defined as Z = ∑ exp(-β E_i); the Boltzmann probability is p_i = exp(-β E_i)/Z; the expected energy is ⟨E⟩ = ∑ p_i E_i; and the discrete entropy is S = -∑ p_i log p_i. Helmholtz free energy is introduced as F = -β^{-1} log Z. These definitions appear in the sibling declarations boltzmannProb, expectedEnergy, boltzmannEntropy, and helmholtzF. The upstream theorem free_energy_identity in BoltzmannDistribution already states the same relation at the level of an abstract System; the present module supplies the concrete finite-sum realization.
proof idea
The declaration is a structure definition whose three fields are populated by direct reference to the already-proved siblings. No local tactics or reductions occur inside HelmholtzRealCert itself; the construction is performed in the one-line wrapper helmholtzRealCert_holds by field assignment from partitionFunction_pos, boltzmannProb_sum_one, and F_eq_E_minus_TS.
why it matters
HelmholtzRealCert supplies the explicit witness that discharges the placeholder free_energy_minimized_at_equilibrium and legendre_transform_structure in the parent module Thermodynamics.FreeEnergy. It is consumed by the theorem helmholtzRealCert_holds, which asserts that the three properties hold simultaneously for any finite discrete spectrum. In the Recognition framework this closes the gap between the abstract free-energy identity and the concrete partition-function sums required for thermodynamic derivations on finite state spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.