IsIdealEnzyme
plain-language theorem explainer
The definition captures the condition under which an enzyme's added J-cost profile exactly negates the bare reaction's activation barrier at the transition state. Catalysis researchers in the Recognition Science framework cite this predicate when establishing zero-barrier corridors and full rate recovery. It is realized as a direct equality between the enzyme's contribution function evaluated at its designated coordinate and the negative activation barrier.
Claim. An enzyme $E$ with transition-state coordinate $x^*$ is ideal when its J-cost contribution satisfies $J_E(x^*) = -(J(x^*) - J(1))$, where $J$ is the base J-cost function.
background
In Recognition Science the J-cost function $J$ assigns a recognition cost to each configuration, with $J(1) = 0$ at the reactant minimum. The activation barrier is therefore the excess cost $J(x^) - J(1)$ at the saddle $x^$. An enzyme is formalized as a structure that supplies an additive J-cost profile together with a designated transition-state coordinate $x^$. The module treats enzymes as J-cost lenses whose geometry is required to focus the ambient field so that the total cost vanishes at $x^$. This definition encodes the complementary-cancellation condition stated in the module documentation: the enzyme contribution at $x^*$ exactly cancels the bare barrier.
proof idea
The definition is a direct predicate. It extracts the enzyme's transition_state_coord, evaluates the jcost_contribution function there, and asserts equality with the negation of activationBarrier applied to the same coordinate. No lemmas or tactics are required; the predicate is the primitive statement of the cancellation.
why it matters
This definition supplies the predicate used by every subsequent catalysis result in the module, including ideal_enzyme_exists, ideal_enzyme_zero_barrier, enzyme_jcost_lens_summary, and rate_enhancement. It realizes the core claim that enzymes act as exact J-cost saddle-point lenses, flattening the transition barrier to zero. The construction is tied to the phi-ladder rung-matching theorem and the specificity result that off-target substrates cannot be cancelled, confirming that zero-cancellation is rung-specific.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.