pith. machine review for the scientific record. sign in
theorem proved term proof

off_target_not_ideal

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 174theorem off_target_not_ideal (enz : Enzyme) (h_ideal : IsIdealEnzyme enz)
 175    (r : ℕ) (h_diff : phi ^ r ≠ enz.transition_state_coord) :
 176    catalyzedBarrier (phi ^ r) enz ≠ 0 := by

proof body

Term-mode proof.

 177  unfold catalyzedBarrier IsIdealEnzyme at *
 178  intro heq
 179  -- The enzyme was optimized for enz.transition_state_coord, not phi^r
 180  -- This would require enz.jcost_contribution (phi^r) = -activationBarrier (phi^r)
 181  -- But the enzyme's contribution at phi^r is -(activationBarrier enz.transition_state_coord)
 182  -- These are unequal by different_rungs_different_barriers (if the rungs differ)
 183  linarith [heq]
 184
 185/-! ## Summary -/
 186
 187/-- Enzymes are exact J-cost saddle-point lenses: ideal enzymes zero the transition barrier. -/

depends on (14)

Lean names referenced from this declaration's body.