higher_temp_faster
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the Arrhenius functional form itself from first principles.
- Does not incorporate quantum-tunneling corrections to the rate.
- Does not address concentration dependence or non-ideal solution effects.
- Assumes a single elementary step with fixed barrier height.
formal statement (Lean)
97theorem higher_temp_faster (A Ea R T1 T2 : ℝ)
98 (hA : A > 0) (hR : R > 0) (hT1 : T1 > 0) (hT2 : T2 > 0) (hT : T1 < T2) (hEa : Ea > 0) :
99 arrheniusRate A Ea R T1 < arrheniusRate A Ea R T2 := by
proof body
Tactic-mode proof.
100 simp only [arrheniusRate]
101 apply mul_lt_mul_of_pos_left _ hA
102 apply exp_lt_exp_of_lt
103 have hRT1 : R * T1 > 0 := mul_pos hR hT1
104 have hRT2 : R * T2 > 0 := mul_pos hR hT2
105 -- -Ea/(R*T1) < -Ea/(R*T2) because T1 < T2 and Ea > 0
106 have h1 : -Ea / (R * T1) < -Ea / (R * T2) := by
107 rw [neg_div, neg_div, neg_lt_neg_iff]
108 apply div_lt_div_of_pos_left hEa hRT1
109 apply mul_lt_mul_of_pos_left hT hR
110 exact h1
111
112/-! ## φ-Scaling of Barriers -/
113
114/-- Characteristic barrier scale: E_coh = φ^(-5) ≈ 0.09 eV. -/