helmholtzRealCert_holds
plain-language theorem explainer
The declaration certifies that the Helmholtz free energy relations hold exactly for any finite discrete system: the partition function is positive, Boltzmann probabilities sum to one, and the free energy equals expected energy minus temperature times entropy. Researchers deriving thermodynamics from information theory or discrete statistical mechanics would cite this result. The proof assembles three supporting lemmas into the required structure via a direct term.
Claim. For every finite nonempty index set $ι$, energy function $E : ι → ℝ$, and $β > 0$, the partition function $Z = ∑_i exp(-β E_i)$ is positive, the probabilities $p_i = exp(-β E_i)/Z$ satisfy $∑ p_i = 1$, and the Helmholtz free energy $F = -log Z / β$ equals the expected energy $⟨E⟩$ minus $T$ times the entropy $S = -∑ p_i log p_i$ with $T = 1/β$.
background
This module supplies concrete proofs for the Helmholtz free energy on finite discrete systems, replacing placeholder assertions in the abstract FreeEnergy module. Key definitions include the partition function $Z = ∑ exp(-β E_i)$, Boltzmann probability $p_i = exp(-β E_i)/Z$, Helmholtz free energy $F = -log Z / β$, expected energy $⟨E⟩ = ∑ p_i E_i$, and entropy $S = -∑ p_i log p_i$ (with the latter two using the normalized Boltzmann weights). The local setting is a finite Fintype with nonempty index set, ensuring all sums are well-defined and the partition function is strictly positive. Upstream results include the free energy identity theorem from BoltzmannDistribution, which derives $F = ⟨E⟩ - TS$ algebraically from the definitions, and the positivity and normalization lemmas proved via direct summation properties.
proof idea
The proof is a term-mode construction of the HelmholtzRealCert structure. It supplies the partition_pos field by direct reference to the partitionFunction_pos lemma, the boltzmann_normalized field by reference to boltzmannProb_sum_one, and the free_energy_identity field by reference to F_eq_E_minus_TS. No additional tactics are required beyond these references.
why it matters
This theorem completes the real proofs for the Helmholtz free energy certificate in the discrete setting, fulfilling the module's goal of replacing trivial placeholders with verified statements. It supports the concrete realization of free energy minimization and the Legendre transform structure asserted in the parent FreeEnergy module. In the broader Recognition framework it grounds thermodynamic identities in finite sums, consistent with the recognition composition law through the J-cost bridge and the underlying partition positivity results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.