Jcost_exp_nonneg

formal source

 115  simp
 116
 117/-- J(e^L) ≥ 0 for all L (AM-GM). -/
 118lemma Jcost_exp_nonneg (L : ℝ) : 0 ≤ Jcost (exp L) :=
 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. -/
 128theorem linJ_matches_harm_def (x L : ℝ) :
 129    linJ x L = ((x - x⁻¹) / 2) * L := rfl
 130
 131/-- **Main Theorem**: The harm linear term is the correct directional derivative.
 132
 133    This justifies using linBondDelta in the harm decomposition. -/
 134theorem harm_linearization_correct (x L : ℝ) (hx : 0 < x) :
 135    -- The linearization linJ captures the first-order behavior of J along exp paths
 136    linJ x L = deriv Jcost x * x * L :=
 137  linJ_eq_derivative_times_x x L hx
 138
 139end Cost
 140end IndisputableMonolith