Jcost_exp_nonneg
The lemma shows that J(e^L) is nonnegative for every real L, a direct consequence of the AM-GM inequality on positive reals. Workers on derivative-based linearizations in the cost module cite it when establishing bounds for the harm function near the identity. The proof reduces immediately to the general nonnegativity lemma by substituting the positive exponential.
claimFor every real number $L$, $J(e^L) ≥ 0$, where $J(x) := (x + x^{-1})/2 - 1$ for $x > 0$.
background
The J-cost function is defined by $J(x) = (x + x^{-1})/2 - 1$ for positive x, which is nonnegative by the AM-GM inequality as shown in the upstream lemma Jcost_nonneg. This module develops derivative formulas for J to support linearizations in the Ethics/Harm module, including the directional derivative linBondDelta(x, L) = ((x - x^{-1})/2) · L. The local setting is the replacement of axioms in harm bounds by explicit Taylor remainders of order O(L²). Upstream results include multiple instances of Jcost_nonneg across modules, each proving nonnegativity via (x - 1)^2 / (2x) ≥ 0 or equivalent AM-GM.
proof idea
The proof is a one-line wrapper applying the general Jcost_nonneg lemma to the argument exp L, which is positive by the exponential function's range.
why it matters in Recognition Science
This result supports the connection between J-cost and harm linearization in the Ethics/Harm module by ensuring nonnegativity of the exponential form. It fills the step needed for quadratic approximations near L=0, as noted in the TODO comment. In the Recognition framework it reinforces the nonnegativity of J that underpins the phi-ladder and mass formulas, though no direct downstream uses are recorded yet.
scope and limits
- Does not prove the quadratic approximation bound for small L
- Does not provide explicit size bounds on J(e^L)
- Does not extend the result to non-real L
formal statement (Lean)
118lemma Jcost_exp_nonneg (L : ℝ) : 0 ≤ Jcost (exp L) :=
proof body
Term-mode proof.
119 Jcost_nonneg (exp_pos L)
120
121-- TODO: For small L, J(e^L) ≈ L²/2 (quadratic)
122-- lemma Jcost_exp_approx (L : ℝ) (hL : |L| ≤ 1) :
123-- |Jcost (exp L) - L ^ 2 / 2| ≤ |L| ^ 3 / 2
124
125/-! ## Connection to Ethics/Harm -/
126
127/-- Matches the linBondDelta definition in Harm.lean. -/