activationBarrier
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.