activationBarrier
The activationBarrier definition supplies the dimensionless activation energy as the excess J-cost at the transition state coordinate x_star relative to the reactant state normalized at 1. Chemists and physicists working in Recognition Science chemistry cite it when deriving Arrhenius rates or enzyme lowering from the J-cost landscape. It is introduced by direct subtraction using the J-cost function together with the auxiliary fact that J(1) vanishes.
claimThe activation energy barrier for a reaction with transition-state coordinate $x^*$ is $E_a(x^*) := J(x^*) - J(1)$, where the J-cost function is $J(x) = (1/2)(x + 1/x) - 1$.
background
In the ActivationEnergy module, barriers emerge from the J-cost landscape of recognition events. The J-cost function is defined by $J(x) = (1/2)(x + 1/x) - 1$ and attains its global minimum of zero at the reactant state $x = 1$. The module states that the transition state corresponds to the maximum J-cost along the reaction coordinate, so the barrier height is exactly the difference $J(x^*) - J(1)$ (dimensionless in RS-native units).
proof idea
The declaration is a one-line definition that subtracts the J-cost at the normalized reactant from the J-cost at the transition state. It relies on the sibling definition of J and the fact that J(1) = 0.
why it matters in Recognition Science
This definition anchors the treatment of chemical kinetics inside the Recognition framework. It is invoked by barrier_nonneg to establish non-negativity, by catalyzedBarrier and IsIdealEnzyme to construct enzyme cancellation, and by enzyme_rung_matching and ideal_enzyme_exists to prove existence of ideal enzymes. It realizes the module claim that Arrhenius form emerges from Boltzmann statistics over the J-cost landscape and that enzyme catalysis reduces J(x*) while preserving reaction energetics. The construction connects to phi-scaling of coherence energies and the eight-tick attempt frequency noted in the module doc.
scope and limits
- Does not compute numerical barrier heights for concrete molecules.
- Does not incorporate explicit temperature or entropy corrections.
- Does not treat multi-step or solvent-mediated reactions.
- Does not derive the pre-exponential factor A from first principles.
Lean usage
theorem barrier_nonneg (x_star : ℝ) (hx : x_star > 0) : activationBarrier x_star ≥ 0 := by simp only [activationBarrier, J_one, sub_zero]; exact J_nonneg x_star hxformal statement (Lean)
51def activationBarrier (x_star : ℝ) : ℝ := J x_star - J 1
proof body
Definition body.
52
53/-- J(1) = 0 (reactant at minimum cost). -/