ideal_enzyme_unit_rate
plain-language theorem explainer
An ideal enzyme satisfying exact J-cost cancellation at the transition state produces a catalyzed rate factor of 1. Researchers modeling enzymatic kinetics within Recognition Science cite this to recover the maximum rate enhancement from zero saddle cost. The proof unfolds the rate definition, substitutes the zero-barrier lemma, and simplifies.
Claim. If an enzyme satisfies the complementary J-cost cancellation condition at its transition-state coordinate, then its catalyzed rate factor equals 1.
background
In this module an enzyme is a structure carrying a J-cost contribution function and a transition-state coordinate off the minimum. The predicate IsIdealEnzyme holds precisely when the enzyme's J-cost at that coordinate equals the negative of the bare activation barrier, flattening the saddle. The catalyzed rate is the Boltzmann factor of the resulting catalyzed barrier, with kT normalized to 1.
proof idea
The proof unfolds catalyzedRate and boltzmannFactor, rewrites the catalyzed barrier to zero via the ideal_enzyme_zero_barrier theorem, and applies simp to obtain the constant 1.
why it matters
This supplies the unit-rate step required by the downstream rate_enhancement theorem, which recovers the full exponential activation-energy factor as the ratio of catalyzed to uncatalyzed rates. It directly implements the module claim that zero saddle cost yields Boltzmann factor 1 and aligns with the J-cost lens mechanism for enzymatic catalysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.