J
plain-language theorem explainer
J-cost function J(x) equals half of (x plus its reciprocal) minus one. Chemists deriving activation barriers and Arrhenius rates from recognition landscapes cite this definition when building J-maxima for transition states. It is supplied as a direct algebraic term that matches the multiplicative cost derived from upstream recognizers.
Claim. $J(x) = ½(x + 1/x) - 1$ for $x > 0$.
background
The Activation Energy Barriers module treats activation energies as maxima of the J-cost landscape along a reaction coordinate. J measures the recognition cost of a positive ratio under the multiplicative recognizer. Upstream, MultiplicativeRecognizerL4.cost defines this as the derivedCost of the comparator, while ObserverForcing.cost states that the cost of any recognition event equals its J-cost.
proof idea
Direct definition that assigns the term (1/2) * (x + 1/x) - 1 to J(x). No lemmas or tactics are invoked; the expression is the primitive term.
why it matters
This definition supplies the core J-cost for the chemistry module, enabling transition states to be identified with J-maxima and the Arrhenius form to emerge from Boltzmann statistics. It realizes the J-uniqueness condition of T5 in the unified forcing chain. Sibling declarations such as activationBarrier and boltzmannFactor apply it to predict phi-scaled barrier heights and enzyme effects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.