boltzmannFactor
plain-language theorem explainer
The Boltzmann factor is defined as exp(-Ea/kT) to give the thermal suppression of rates over an activation barrier in the J-cost landscape. Chemists deriving Arrhenius kinetics from Recognition Science would cite this when linking barrier heights to observed reaction speeds. It is introduced via a direct one-line definition using the real exponential.
Claim. The Boltzmann factor is given by $e^{-E_a/kT}$, where $E_a$ is the activation energy and $kT$ is the thermal energy scale.
background
The ActivationEnergy module treats chemical barriers as maxima of the J-cost function along a reaction coordinate, with the transition state at the peak J value. The Boltzmann factor then supplies the relative probability of occupying that state under thermal statistics, recovering the Arrhenius form k = A exp(-Ea/RT). Upstream, A is the active edge count per tick (IntegrationGap.A and Masses.Anchor.A), while parallel Boltzmann factors in EnzymeCatalysis and ShannonEntropy connect entropy to rate suppression.
proof idea
This is a one-line definition: boltzmannFactor Ea kT := exp(-Ea/kT). No lemmas or tactics are applied; the expression is used verbatim in downstream rate ratios.
why it matters
The definition feeds enzyme_enhances_rate and rateEnhancement, which establish that barrier reduction yields a multiplicative rate gain via the ratio of two Boltzmann factors. It realizes the module claim that Arrhenius kinetics emerges from J-cost statistics, connecting to the eight-tick octave for attempt frequency A and phi-scaling of coherence energy E_coh. It also bridges to the ShannonEntropy treatment of thermodynamic entropy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.