 102
 103/-- The remainder term after linearization:
 104    rem(x, L) = J(x·e^L) - J(x) - linJ(x, L) -/
 105noncomputable def remJ (x L : ℝ) : ℝ :=
 106  Jcost (x * exp L) - Jcost x - linJ x L
 107
 108-- TODO: Quadratic Remainder Bound
 109-- theorem remJ_quadratic_bound (x : ℝ) (hx : 0 < x) :
 110--     ∃ C > 0, ∀ L, |L| ≤ 1 → |remJ x L| ≤ C * L ^ 2
 111
 112/-- At unit multiplier, the remainder equals J(e^L) - J(1) - 0 = J(e^L). -/
 113lemma remJ_unit (L : ℝ) : remJ 1 L = Jcost (exp L) := by
 114  unfold remJ linJ Jcost
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.