J_transition
plain-language theorem explainer
J_transition supplies the J-cost evaluated at the transition-state coordinate x_star by direct substitution into the core J function. Reaction-rate models in the Recognition Science chemistry setting cite this alias to mark the height of the activation barrier on the cost landscape. The definition is a one-line alias with no lemmas or reductions required.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. The transition-state cost is then $J(x^*)$.
background
The Activation Energy Barriers module treats chemical activation energies as maxima of the J-cost landscape along a reaction coordinate. The referenced J function is defined by $J(x) = (1/2)(x + 1/x) - 1$ and quantifies recognition cost for any real configuration x. The local J_transition extracts the value of this function at the transition-state point x_star, which the module documentation identifies as the J-maximum that sets the barrier height.
proof idea
One-line wrapper that applies the core J function to the supplied argument x_star.
why it matters
The definition supplies the transition-state cost term required by PathAction and modal_distance in the modal geometry and actualization modules. It implements the module claim that the transition state is the J-maximum, thereby enabling the derivation of Arrhenius rates from Boltzmann statistics over the J-cost surface and the phi-scaling of barrier heights. It connects directly to the eight-tick octave through the pre-exponential attempt frequency and feeds the downstream lemmas on determined properties and identity preference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.