Jcost_exp_nonneg
plain-language theorem explainer
The lemma shows that J(e^L) is nonnegative for every real L. Workers on cost linearization in Recognition Science cite it when deriving harm bounds or consent conditions from the derivative theory. The proof is a one-line wrapper that feeds the positivity of exp L into the general Jcost non-negativity result.
Claim. For every real number $L$, $J(e^L) ≥ 0$, where $J(x) = (x + x^{-1})/2 - 1$.
background
The J-cost function is defined by $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Its non-negativity follows from the AM-GM inequality $x + x^{-1} ≥ 2$, which rearranges directly to $J(x) ≥ 0$. The Cost.Derivative module supplies the derivative formulas needed to replace axioms in the Ethics/Harm module, including the linearization $linBondDelta(x, L) = ((x - x^{-1})/2) · L$ and quadratic remainder bounds. Upstream lemmas establish the same non-negativity statement in multiple modules (Cost, Gravity, Navier-Stokes) via the representation $J(x) = (x-1)^2/(2x)$ or direct AM-GM application.
proof idea
One-line wrapper that applies the general Jcost_nonneg lemma to the fact that exp L > 0, supplied by the standard positivity of the exponential.
why it matters
It supplies a concrete instance of J-cost non-negativity at exponential arguments, supporting the derivative theory that lets linBondDelta serve as the correct linearization for harm bounds. This step helps close the path from the Recognition Composition Law to consent derivations in the Ethics module. No downstream uses are recorded yet, but the result sits inside the chain that replaces harm axioms with theorems derived from the J-cost derivative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.