J_reactant

formal source

  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 -/