arrheniusRate
plain-language theorem explainer
The definition supplies the standard Arrhenius rate constant k = A exp(-Ea/(R T)) inside the Recognition Science account of chemical kinetics. Modelers of activation barriers in J-cost landscapes would cite it when stating rate monotonicities. It is introduced as a direct algebraic expression that encodes the Boltzmann factor over the transition-state maximum.
Claim. $k = A_0 e^{-E_a/(R T)}$ where $A_0$ is the pre-exponential factor, $E_a$ the activation energy, $R$ the gas constant, and $T$ the absolute temperature.
background
The Chemistry.ActivationEnergy module derives activation barriers from maxima of the J-cost function along the reaction coordinate. The transition state is the configuration of highest J-cost, and the rate follows from Boltzmann statistics exp(-J) over that landscape. Upstream, the module imports the fundamental period T as a natural number from Breath1024 and the active edge count A as unity from IntegrationGap, both of which normalize the coherence energy E_coh = phi^{-5}.
proof idea
The declaration is a direct definition that composes the exponential with the negative ratio of activation energy to the product of gas constant and temperature, scaled by the prefactor. No lemmas or tactics are invoked; the expression is taken as primitive and then referenced by the two monotonicity theorems in the same module.
why it matters
It anchors the two downstream theorems higher_barrier_slower and higher_temp_faster that establish monotonic dependence of rate on barrier height and temperature. The module documentation states that the Arrhenius equation emerges from Boltzmann statistics over the J-cost landscape and that barrier heights scale with phi powers of coherence energy, thereby connecting chemical kinetics to the Recognition Composition Law and the eight-tick octave. It leaves open the explicit derivation of the prefactor from attempt frequencies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.