higher_temp_faster
plain-language theorem explainer
The theorem shows that the Arrhenius reaction rate constant strictly increases with temperature when the pre-factor, gas constant, temperatures, and activation energy are all positive. Kinetic modelers working inside the Recognition Science J-cost framework cite it to recover the observed temperature dependence of rates from the underlying Boltzmann statistics over the transition-state barrier. The proof is a short tactic sequence that unfolds the rate definition, applies positivity-preserving multiplication and exponential monotonicity, then 1
Claim. Let $A, E_a, R, T_1, T_2$ be real numbers satisfying $A > 0$, $R > 0$, $T_1 > 0$, $T_2 > 0$, $T_1 < T_2$, and $E_a > 0$. Then the Arrhenius rate at the lower temperature is strictly smaller: $A · exp(-E_a / (R T_1)) < A · exp(-E_a / (R T_2))$.
background
The module treats activation barriers as maxima of the J-cost function along a reaction coordinate; the transition state is the point of highest J-cost, and the barrier height $E_a$ is identified with that maximum. The Arrhenius rate is defined directly as $A · exp(-E_a / (R T))$, recovering the classical form from Boltzmann weighting over the J-cost landscape. Upstream results supply the positivity lemmas for multiplication and division together with the exponential comparison rule used in the comparison of the two exponents.
proof idea
The tactic proof first simplifies the goal to the explicit rate expression, then applies mul_lt_mul_of_pos_left to reduce the inequality to a comparison of the two exponentials. It next invokes exp_lt_exp_of_lt, which requires showing the exponents satisfy -Ea/(R T1) < -Ea/(R T2). Positivity of R T1 and R T2 is recorded, the negation is removed via neg_lt_neg_iff, and the resulting division inequality is discharged by div_lt_div_of_pos_left followed by mul_lt_mul_of_pos_left on the temperatures.
why it matters
The result closes the temperature-dependence step inside the CH-017 activation-energy development, confirming that the J-cost-derived Arrhenius form reproduces the classical observation that rates rise with temperature. It sits downstream of the arrheniusRate definition and the J-cost maximum characterization; no downstream uses are recorded yet, but the lemma is required for any later quantitative comparison of catalyzed versus uncatalyzed barriers or for phi-scaled barrier heights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.