ideal_enzyme_zero_barrier
plain-language theorem explainer
An ideal enzyme cancels the transition-state J-cost exactly, forcing the catalyzed barrier to zero. Researchers deriving maximum enzymatic rate enhancements from the J-cost lens model cite this when computing Boltzmann factors for catalyzed reactions. The term proof unfolds the barrier sum definition and applies linear arithmetic directly to the cancellation hypothesis.
Claim. If an enzyme satisfies the complementary J-cost cancellation condition at its transition-state coordinate $x^*$, then the total catalyzed J-cost barrier at $x^*$ equals zero.
background
In this module an enzyme is a structure that supplies a J-cost contribution function together with a transition-state coordinate. The ideal enzyme predicate requires that the contribution at the transition-state coordinate exactly equals the negative of the bare activation barrier. The catalyzed barrier is defined as the sum of the bare activation barrier and the enzyme contribution. The module develops enzymes as J-cost lenses whose folded topology cancels the reaction saddle, with the zero-barrier case as the ideal limit. The module documentation states that an enzyme acts as a J-cost lens focusing the ambient field to cancel the saddle point at the active site.
proof idea
The proof is a one-line term wrapper. It unfolds the definitions of the catalyzed barrier and the ideal enzyme predicate, then invokes linear arithmetic on the equality supplied by the hypothesis.
why it matters
This theorem supplies the zero-barrier step required by the enzyme J-cost lens summary theorem and the ideal enzyme unit rate theorem. It realizes the complementary cancellation step in the Recognition Science treatment of enzymes as saddle-point stabilizers, consistent with phi-ladder scaling of transition-state barriers. It closes the local claim that ideal enzymes produce zero-cost corridors through transition states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.