IndisputableMonolith.Chemistry.ActivationEnergy

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Activation Energy Barriers (CH-017)
   6
   7Activation energy barriers in chemical reactions emerge from J-cost landscape.
   8
   9## RS Mechanism
  10
  111. **Transition State as J-Maximum**: The transition state corresponds to the
  12   maximum J-cost along the reaction coordinate. J(x*) is the activation barrier.
  13
  142. **Arrhenius Form from Boltzmann**: The Arrhenius equation k = A·exp(-Ea/RT)
  15   emerges from Boltzmann statistics over the J-cost landscape.
  16
  173. **φ-Scaling of Barriers**: Characteristic barrier heights scale with φ powers
  18   of the coherence energy E_coh.
  19
  204. **Enzyme Catalysis**: Enzymes lower activation energy by reshaping the
  21   J-cost landscape, reducing J(x*) while preserving reaction energetics.
  22
  23## Key Predictions
  24
  25- Arrhenius equation emerges from J-cost
  26- Ea scales with bond strength (φ-related)
  27- Enzyme catalysis reduces J(x*) by stabilizing transition state
  28- Pre-exponential factor A relates to attempt frequency (8-tick)
  29-/
  30
  31namespace IndisputableMonolith
  32namespace Chemistry
  33namespace ActivationEnergy
  34
  35noncomputable section
  36
  37open Constants Real
  38
  39/-! ## J-Cost Landscape -/
  40
  41/-- J-cost function: J(x) = ½(x + 1/x) - 1 -/
  42def J (x : ℝ) : ℝ := (1/2) * (x + 1/x) - 1
  43
  44/-- J-cost at reactant (normalized to x = 1). -/
  45def J_reactant : ℝ := J 1
  46
  47/-- J-cost at transition state (x = x*). -/
  48def J_transition (x_star : ℝ) : ℝ := J x_star
  49
  50/-- Activation energy (dimensionless) = J(x*) - J(reactant). -/
  51def activationBarrier (x_star : ℝ) : ℝ := J x_star - J 1
  52
  53/-- J(1) = 0 (reactant at minimum cost). -/
  54theorem J_one : J 1 = 0 := by simp only [J]; ring
  55
  56/-- J(x) ≥ 0 for all x > 0.
  57    Proof: J(x) = ½(x + 1/x) - 1 ≥ 0 follows from AM-GM: x + 1/x ≥ 2. -/
  58theorem J_nonneg (x : ℝ) (hx : x > 0) : J x ≥ 0 := by
  59  -- AM-GM: For x > 0, x + 1/x ≥ 2 follows from (x - 1)² ≥ 0 when x = 1.
  60  -- More generally, use x + 1/x - 2 = (x - 1)²/x ≥ 0.
  61  simp only [J]
  62  have hx_ne : x ≠ 0 := ne_of_gt hx
  63  have h_key : x + 1/x - 2 = (x - 1)^2 / x := by field_simp; ring
  64  have h_sq_nonneg : (x - 1)^2 ≥ 0 := sq_nonneg _
  65  have h_div_nonneg : (x - 1)^2 / x ≥ 0 := div_nonneg h_sq_nonneg (le_of_lt hx)
  66  have h_am_gm : x + 1/x ≥ 2 := by linarith [h_key, h_div_nonneg]
  67  linarith
  68
  69/-- Activation barrier is non-negative. -/
  70theorem barrier_nonneg (x_star : ℝ) (hx : x_star > 0) :
  71    activationBarrier x_star ≥ 0 := by
  72  simp only [activationBarrier, J_one, sub_zero]
  73  exact J_nonneg x_star hx
  74
  75/-! ## Arrhenius Equation -/
  76
  77/-- Boltzmann factor: exp(-Ea / kT). -/
  78def boltzmannFactor (Ea kT : ℝ) : ℝ := exp (-Ea / kT)
  79
  80/-- Arrhenius rate constant: k = A · exp(-Ea / RT). -/
  81def arrheniusRate (A Ea R T : ℝ) : ℝ := A * exp (-Ea / (R * T))
  82
  83/-- Higher barrier → lower rate (Arrhenius law). -/
  84theorem higher_barrier_slower (A Ea1 Ea2 R T : ℝ)
  85    (hA : A > 0) (hR : R > 0) (hT : T > 0) (hE : Ea1 < Ea2) :
  86    arrheniusRate A Ea2 R T < arrheniusRate A Ea1 R T := by
  87  simp only [arrheniusRate]
  88  apply mul_lt_mul_of_pos_left _ hA
  89  apply exp_lt_exp_of_lt
  90  have hRT : R * T > 0 := mul_pos hR hT
  91  have h1 : -Ea2 / (R * T) < -Ea1 / (R * T) := by
  92    apply div_lt_div_of_pos_right _ hRT
  93    linarith
  94  exact h1
  95
  96/-- Higher temperature → higher rate (Arrhenius law). -/
  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
 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. -/
 115def E_coh : ℝ := phi ^ (-5 : ℝ)
 116
 117/-- Barrier height for n-th ladder rung: E_coh · φ^n. -/
 118def barrierLadder (n : ℤ) : ℝ := E_coh * phi ^ n
 119
 120/-- Hydrogen bond barriers are at the E_coh scale. -/
 121theorem hbond_barrier_scale : barrierLadder 0 = E_coh := by
 122  simp only [barrierLadder, zpow_zero, mul_one]
 123
 124/-- Covalent bond barriers are higher (n > 0). -/
 125theorem covalent_barrier_higher : barrierLadder 1 > barrierLadder 0 := by
 126  simp only [barrierLadder, zpow_one, zpow_zero, mul_one]
 127  have h_phi_gt_1 : phi > 1 := one_lt_phi
 128  have h_E_coh_pos : E_coh > 0 := by
 129    simp only [E_coh]
 130    exact rpow_pos_of_pos phi_pos _
 131  nlinarith
 132
 133/-! ## Enzyme Catalysis -/
 134
 135/-- Enzymatic transition state stabilization factor. -/
 136def catalyticFactor (E_uncat E_cat : ℝ) : ℝ := E_uncat / E_cat
 137
 138/-- Catalysis means lower activation energy. -/
 139theorem catalysis_lowers_barrier (E_uncat E_cat : ℝ)
 140    (h_cat_lower : E_cat < E_uncat) (h_pos : E_cat > 0) :
 141    catalyticFactor E_uncat E_cat > 1 := by
 142  simp only [catalyticFactor, gt_iff_lt, one_lt_div h_pos]
 143  exact h_cat_lower
 144
 145/-- Rate enhancement from catalysis. -/
 146def rateEnhancement (E_uncat E_cat kT : ℝ) : ℝ :=
 147  boltzmannFactor E_cat kT / boltzmannFactor E_uncat kT
 148
 149/-- Enzyme rate enhancement is > 1 when barrier is lowered. -/
 150theorem enzyme_enhances_rate (E_uncat E_cat kT : ℝ)
 151    (h_cat_lower : E_cat < E_uncat) (h_kT_pos : kT > 0) :
 152    rateEnhancement E_uncat E_cat kT > 1 := by
 153  simp only [rateEnhancement, boltzmannFactor]
 154  -- exp(-E_cat/kT) / exp(-E_uncat/kT) = exp((-E_cat + E_uncat)/kT) = exp((E_uncat - E_cat)/kT)
 155  rw [← Real.exp_sub]
 156  have h_diff_pos : (E_uncat - E_cat) / kT > 0 := by
 157    apply div_pos _ h_kT_pos
 158    linarith
 159  have h_simp : (- E_cat / kT) - (-E_uncat / kT) = (E_uncat - E_cat) / kT := by ring
 160  rw [h_simp]
 161  exact Real.one_lt_exp_iff.mpr h_diff_pos
 162
 163/-! ## Attempt Frequency (Pre-exponential Factor) -/
 164
 165/-- The pre-exponential factor A relates to molecular vibrations.
 166    For typical reactions, A ≈ 10^13 s^-1 (vibrational frequency). -/
 167def attemptFrequency : ℝ := 1e13
 168
 169/-- The 8-tick period τ = 8 / (E_coh / ℏ) gives a characteristic time. -/
 170def eightTickPeriod : ℝ := 8 / attemptFrequency
 171
 172/-- Attempt frequency is related to 8-tick structure. -/
 173theorem attempt_freq_8tick : attemptFrequency = 8 / eightTickPeriod := by
 174  simp only [eightTickPeriod]
 175  field_simp
 176
 177end
 178
 179end ActivationEnergy
 180end Chemistry
 181end IndisputableMonolith
 182