rate_enhancement
plain-language theorem explainer
For an ideal enzyme the catalyzed-to-uncatalyzed rate ratio equals the exponential of the bare transition-state barrier, recovering the full activation energy as a multiplicative factor. Chemists working on enzymatic specificity or phi-ladder rate models would cite the result. The proof is a short term-mode reduction that substitutes the ideal-enzyme unit-rate lemma and rewrites the Boltzmann-factor definitions.
Claim. Let $enz$ be an enzyme whose J-cost contribution exactly cancels the bare activation barrier at its transition-state coordinate $x^*$. Then the ratio of catalyzed rate to uncatalyzed rate at $x^*$ satisfies $k_ cat / k_ uncat(x^*) = exp(uncatalyzed barrier at $x^*$).
background
The EnzymeCatalysis module treats enzymes as J-cost lenses whose folded topology supplies an additive inverse to the reaction saddle. An Enzyme structure carries a J-cost contribution function and a transition-state coordinate; IsIdealEnzyme is the proposition that this contribution at the transition state equals the negative of the bare activation barrier, producing a zero-cost corridor. The module setting is the Recognition Science claim that enzymes achieve complementary cancellation rather than classical lowering of activation energy.
proof idea
The term proof first rewrites the catalyzed rate via the ideal_enzyme_unit_rate theorem, which replaces it by 1. It then unfolds uncatalyzedRate and boltzmannFactor, rewrites the reciprocal using one_div, and applies Real.exp_neg to obtain the positive exponential of the uncatalyzed barrier.
why it matters
The theorem supplies the explicit rate-enhancement identity required by the module's core claim that zero saddle cost recovers the full activation energy. It closes the catalytic-rate step in the J-cost lens argument and supports the downstream specificity result that only matching phi-ladder rungs permit exact cancellation. The identity sits inside the broader Recognition Science treatment of activation barriers via the Boltzmann factor and the phi-scaling of active-site rungs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.