Enzyme
plain-language theorem explainer
An enzyme is formalized as a structure with a J-cost contribution function from reaction coordinate to real, a transition-state coordinate distinct from 1, and the associated inequality. Researchers modeling catalysis via J-cost cancellation in Recognition Science would cite this to construct rate-enhancement and barrier-zeroing results. The declaration is a direct structure definition with three fields and no computational content.
Claim. An enzyme consists of a function $j : ℝ → ℝ$ giving the J-cost contribution at each reaction coordinate, a real number $x^*$ for the transition-state coordinate, and the condition $x^* ≠ 1$.
background
J-cost is the derived cost function induced by a multiplicative recognizer on positive ratios, equivalently the cost of any recognition event. The module develops enzymes as J-cost lenses whose folded topology cancels the saddle at the transition state, producing a zero-cost corridor. Upstream results establish that cost is non-negative and that primitive distinctions yield four structural conditions on forcing chains.
proof idea
The declaration is a direct structure definition introducing the J-cost contribution map, the transition-state coordinate, and the off-minimum inequality. No lemmas or tactics are applied; it supplies the type used by downstream definitions such as catalyzedBarrier and catalyzedRate.
why it matters
This structure supplies the type for all enzyme catalysis results in the module, including enzyme_jcost_lens_summary (existence of ideal enzymes that zero the barrier) and enzyme_rung_matching (phi-ladder complementarity). It realizes the Q19 claim that enzymes act as exact J-cost saddle-point lenses, aligning with the phi-ladder mass formula and the eight-tick octave. It touches the open question of how precise complementarity is enforced for off-target specificity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.