boltzmannProb
plain-language theorem explainer
Boltzmann probability for energy level i is the normalized exponential weight exp(-β E_i) divided by the partition sum Z. Researchers working on variational inference and equilibrium thermodynamics cite this when minimizing free energy functionals over probability distributions. The definition is a direct one-line normalization using the already-defined partition function.
Claim. For a finite index set ι with energy function E : ι → ℝ and inverse temperature β, the probability of level i is p_i = e^{-β E_i} / Z(β) where Z(β) = ∑_j e^{-β E_j}.
background
The HelmholtzReal module supplies real proofs for a finite discrete system: the partition function is Z(β) = ∑_i exp(-β E_i) and the free energy is F = -log Z / β. The Boltzmann probability is the normalized factor that realizes the equilibrium distribution minimizing the functional sum p_i E_i - T H[p]. Upstream results include the same-module partitionFunction definition and the general partitionFunction from BoltzmannDistribution and PartitionFunction, which handle weighted sums of Boltzmann factors.
proof idea
This is a definition that directly divides the Boltzmann factor Real.exp (-β * E i) by the partitionFunction E β. No tactics are used; it is an abbrev-style definition.
why it matters
This definition supplies the reference distribution for boltzmannDist and the minimization theorem boltzmann_minimizes_vfe in VariationalFreeEnergyFromRCL, which establishes the Gibbs inequality bound. It also feeds boltzmannEntropy, expectedEnergy, and the identity F = E - T S. In the Recognition framework it grounds the thermodynamic content of the free-energy minimization on the discrete phi-ladder energies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.