J_nonneg
plain-language theorem explainer
J(x) is non-negative for every positive real x, following from the AM-GM inequality on the definition J(x) = (x + 1/x)/2 - 1. Chemists modeling reaction kinetics inside the Recognition Science J-cost framework would cite this to guarantee that activation barriers remain positive. The proof is a short tactic sequence that algebraically rewrites the expression, invokes non-negativity of squares, and closes with linarith.
Claim. For every real number $x > 0$, $J(x) := 1/2(x + 1/x) - 1$ satisfies $J(x) ≥ 0$.
background
The Chemistry.ActivationEnergy module treats activation barriers as maxima of the J-cost landscape along reaction coordinates. The J-cost function is defined by J(x) = 1/2(x + 1/x) - 1. This setting implements the RS mechanism in which transition states are J-maxima, Arrhenius rates emerge from Boltzmann statistics over the J-landscape, and barrier heights scale with φ-powers of coherence energy. The local result rests on the elementary real-analytic properties of J rather than on the imported foundational structures such as PrimitiveDistinction or MechanismDesignFromSigma.
proof idea
The tactic proof first applies simp to unfold the definition of J. It then proves the algebraic identity x + 1/x - 2 = (x-1)^2 / x by field_simp and ring. Non-negativity of (x-1)^2 is immediate from sq_nonneg; division by positive x preserves the sign by div_nonneg. Linarith lifts the inequality to x + 1/x ≥ 2, which rearranges directly to J(x) ≥ 0.
why it matters
The theorem guarantees that activation barriers extracted from the J-cost landscape are non-negative, thereby licensing the Arrhenius form k = A exp(-Ea/RT) inside the module. It instantiates the J-uniqueness property (T5) of the forcing chain, where J(x) = (x + x^{-1})/2 - 1. No downstream theorems are recorded, yet the result is a prerequisite for barrier_nonneg and rate calculations that follow in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.