J_one
plain-language theorem explainer
J(1) equals zero by direct evaluation of the cost function at the normalized reactant. Chemists modeling reaction barriers via J-cost landscapes cite this to fix the zero of the energy scale before deriving Arrhenius rates or enzyme effects. The term proof unfolds the definition and reduces the resulting expression to zero by ring arithmetic.
Claim. $J(1) = 0$, where $J(x) = ½(x + x^{-1}) - 1$ for $x > 0$.
background
The Activation Energy module models chemical barriers as maxima of the J-cost landscape along a reaction coordinate. J is defined by $J(x) = ½(x + 1/x) - 1$, which satisfies the Recognition Composition Law and reaches its global minimum at the reactant state $x = 1$ by construction. The module builds Arrhenius forms and enzyme catalysis on this zero point, with pre-exponential factors tied to the eight-tick octave.
proof idea
One-line term proof that applies simp only on the definition of J followed by the ring tactic to obtain the identity.
why it matters
This anchors every barrier calculation in the chemistry module and feeds barrier_nonneg, different_rungs_different_barriers, ideal_enzyme_exists, and matched_at_safe. It realizes the T5 J-uniqueness at the fixed point and supplies the zero required for phi-ladder scaling of activation energies and for the vacuum J-cost result in string theory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.