ideal_enzyme_exists
plain-language theorem explainer
For any real transition coordinate x_star there exists an enzyme whose added J-cost profile exactly cancels the bare activation barrier at that point. Recognition Science models of catalytic specificity and rate enhancement cite this existence result. The proof splits on whether x_star equals 1, builds a zero-contribution enzyme when the barrier vanishes and an inverting enzyme otherwise, then closes by direct simplification against the ideal-enzyme predicate.
Claim. For every real number $x_*$, there exists an enzyme whose transition-state coordinate equals $x_*$ and whose J-cost contribution at $x_*$ equals the negative of the activation barrier $J(x_*) - J(1)$.
background
An enzyme is a structure carrying a J-cost contribution function and a distinguished transition-state coordinate $x_$ that is required to lie off the reactant minimum at 1. The predicate IsIdealEnzyme holds precisely when the enzyme's contribution at $x_$ equals the negative of the activation barrier, which itself is defined as $J(x_) - J(1)$. The upstream lemma J_one establishes $J(1) = 0$, so the barrier reduces to $J(x_)$ and the ideal condition becomes exact cancellation of the saddle-point cost. The module frames enzymes as J-cost lenses whose topology supplies the additive inverse of the reaction's transition-state cost, producing a zero-cost corridor.
proof idea
The tactic proof performs case analysis on the predicate $x_* = 1$. When equality holds the barrier is already zero, so the construction supplies the constant-zero contribution function together with the supplied coordinate and closes by simplification using IsIdealEnzyme, activationBarrier and J_one. When $x_* ≠ 1$ the construction supplies the contribution function that returns the exact negative of the activation barrier at the given coordinate and again closes by simplification against IsIdealEnzyme.
why it matters
The result supplies the existence half of the core claim in the module that enzymes act as exact J-cost saddle-point lenses. It is invoked directly by the downstream summary theorem enzyme_jcost_lens_summary, which strengthens the statement to include the additional fact that the catalyzed barrier vanishes. Within the Recognition framework the construction realizes the complementary-cancellation step required for the phi-scaled active-site geometry and the consequent Boltzmann rate enhancement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.