boltzmannFactor
plain-language theorem explainer
The Boltzmann factor for an energy level with energy E and degeneracy g computes the weighted contribution g exp(-beta E) to the partition function. Chemists modeling activation barriers and statistical mechanicians deriving distributions from J-cost cite it when constructing probabilities under fixed total recognition cost. The definition is a direct one-line algebraic expression using Real.exp on the scaled energy.
Claim. For an energy level with energy $E$ and degeneracy $g > 0$, the Boltzmann factor at inverse temperature $beta$ is $g exp(-beta E)$.
background
EnergyLevel is a structure that pairs a real energy value with a positive natural-number degeneracy counting the microstates at that energy. The module derives the Boltzmann distribution from Recognition Science's J-cost functional, where states are selected to maximize microstate count subject to a fixed total J-cost constraint; the Lagrange multiplier for that constraint is identified with beta = 1/kT. Upstream results supply analogous exponential factors in activation-energy and enzyme-catalysis calculations, together with the link between thermodynamic and Shannon entropy.
proof idea
The definition is a one-line wrapper that multiplies the degeneracy field by the real exponential of the negative product of beta and the energy field.
why it matters
This supplies the core weighting term used by downstream results such as rateEnhancement and catalyzedRate in enzyme kinetics. It realizes the THERMO-001 derivation of statistical mechanics from J-cost, connecting to the Recognition Composition Law and the emergence of temperature as the derivative of total cost with respect to entropy. The same module later assembles the partition function from repeated applications of this factor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.