jcost_exp_nonneg
plain-language theorem explainer
The result shows that J-cost of any real exponential is non-negative. Workers on the J-cost identities and the UnifiedForcingChain cite it when assembling the certificate for the cosh representation. The short proof applies the cosh-form lemma and invokes standard exponential inequalities to reach the conclusion by non-linear arithmetic.
Claim. For every real number $y$, $0 ≤ J(e^y)$ where $J(x) := (x + x^{-1})/2 - 1$.
background
The module defines the non-linear cosh form of J-cost as J(e^y) = (e^y + e^{-y})/2 - 1, the expression that appears in the strong-field Regge action. It lists four properties: vanishing only at y = 0, symmetry under y to -y, strict positivity off zero, and non-negativity in all cases. The upstream theorem jcost_exp_cosh_form establishes the equality itself by reducing Jcost via Jcost_eq_sq, applying exp_neg, and simplifying with field_simp and ring.
proof idea
The proof is a short tactic sequence. It rewrites the goal with jcost_exp_cosh_form. It introduces the two facts Real.add_one_le_exp y and Real.add_one_le_exp (-y). Non-linear arithmetic then combines these with Real.exp_pos y and Real.exp_pos (-y) to close the inequality.
why it matters
This theorem supplies the nonneg field inside the jCostCoshCert definition that aggregates the complete set of properties for the cosh form. It fills the fourth item in the module's enumerated list of key properties for the Beltracchi Response §5. In the Recognition framework it supports the J-uniqueness step T5 by guaranteeing the cost function stays non-negative away from the fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.