162 unfold activationBarrier J_one J 163 simp only [sub_zero] 164 intro heq 165 have h1 : (0 : ℝ) < phi ^ r₁ := pow_pos phi_pos r₁ 166 have h2 : (0 : ℝ) < phi ^ r₂ := pow_pos phi_pos r₂ 167 -- If ½(φ^r₁ + φ^{-r₁}) = ½(φ^r₂ + φ^{-r₂}) then φ^r₁ = φ^r₂ 168 -- (J is strictly convex and symmetric about 1, so injective on (1,∞)) 169 have := pow_left_injective₀ (ne_of_gt phi_pos) h 170 simp only [heq] at this 171 exact h (this rfl) 172 173/-- A single-rung enzyme is an imperfect catalyst for a different-rung reaction. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.