IndisputableMonolith.Cost.Derivative

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# J-Cost Derivative Theory
   6
   7This module provides the key derivative formulas for the J-cost function
   8that enable replacing axioms in the Ethics/Harm module.
   9
  10## Main Results
  11
  121. `deriv_Jcost_eq`: d/dx J(x) = (1 - x⁻²)/2 for x > 0
  132. `linBondDelta_is_derivative`: The linearized bond delta equals the directional derivative
  143. `remJ_quadratic`: Quadratic remainder bound for Taylor expansion
  15
  16These results establish that:
  17- linBondDelta(x, L) = ((x - x⁻¹)/2) · L is the correct linearization
  18- The remainder is O(L²), enabling consent derivation from harm bounds
  19-/
  20
  21namespace IndisputableMonolith
  22namespace Cost
  23
  24open Real
  25
  26/-! ## J-cost Basic Properties -/
  27
  28/-- J(x) = (x + x⁻¹)/2 - 1 is differentiable for x > 0. -/
  29lemma differentiableAt_Jcost (x : ℝ) (hx : 0 < x) : DifferentiableAt ℝ Jcost x := by
  30  have hxne : x ≠ 0 := ne_of_gt hx
  31  unfold Jcost
  32  apply DifferentiableAt.sub
  33  · apply DifferentiableAt.div_const
  34    apply DifferentiableAt.add differentiableAt_id
  35    exact differentiableAt_inv hxne
  36  · exact differentiableAt_const 1
  37
  38/-- The derivative of J at x equals (1 - x⁻²)/2.
  39
  40    Proof: J(x) = (x + x⁻¹)/2 - 1
  41    J'(x) = d/dx[(x + x⁻¹)/2 - 1] = (1 + (-x⁻²))/2 = (1 - x⁻²)/2
  42
  43    **Technical note**: This is standard calculus, using:
  44    - d/dx[x] = 1
  45    - d/dx[x⁻¹] = -x⁻² -/
  46lemma deriv_Jcost_eq (x : ℝ) (hx : 0 < x) :
  47    deriv Jcost x = (1 - x⁻¹ ^ 2) / 2 := by
  48  have hxne : x ≠ 0 := ne_of_gt hx
  49  -- J(x) = (x + x⁻¹)/2 - 1
  50  -- J'(x) = (1 + d/dx[x⁻¹])/2 = (1 - x⁻²)/2
  51  -- Use HasDerivAt to compute the derivative
  52  have h_inv : HasDerivAt (·⁻¹) (-(x ^ 2)⁻¹) x := hasDerivAt_inv hxne
  53  have h_id : HasDerivAt id 1 x := hasDerivAt_id x
  54  have h_add : HasDerivAt (fun y => y + y⁻¹) (1 + -(x ^ 2)⁻¹) x :=
  55    h_id.add h_inv
  56  have h_div : HasDerivAt (fun y => (y + y⁻¹) / 2) ((1 + -(x ^ 2)⁻¹) / 2) x :=
  57    h_add.div_const 2
  58  have h_sub : HasDerivAt (fun y => (y + y⁻¹) / 2 - 1) ((1 + -(x ^ 2)⁻¹) / 2) x :=
  59    h_div.sub_const 1
  60  -- h_sub gives: HasDerivAt Jcost ((1 - x⁻²) / 2) x
  61  have h_eq : (1 + -(x ^ 2)⁻¹) / 2 = (1 - x⁻¹ ^ 2) / 2 := by
  62    have h1 : (x ^ 2)⁻¹ = x⁻¹ ^ 2 := by
  63      rw [pow_two, pow_two, mul_inv_rev]
  64    rw [h1]
  65    ring
  66  rw [h_eq] at h_sub
  67  exact h_sub.deriv
  68
  69/-! ## Linearized Bond Delta -/
  70
  71/-- The linearized per-bond delta for J under log-strain L at base x. -/
  72noncomputable def linJ (x L : ℝ) : ℝ := ((x - x⁻¹) / 2) * L
  73
  74/-- At unit multiplier (x=1), the linear term vanishes. -/
  75lemma linJ_unit (L : ℝ) : linJ 1 L = 0 := by simp [linJ]
  76
  77/-- The key identity connecting linJ to the derivative:
  78    linJ(x, L) = J'(x) · x · L
  79
  80    Algebraic identity: (x - x⁻¹)/2 = ((1 - x⁻²)/2) · x -/
  81theorem linJ_eq_derivative_times_x (x L : ℝ) (hx : 0 < x) :
  82    linJ x L = deriv Jcost x * x * L := by
  83  have hxne : x ≠ 0 := ne_of_gt hx
  84  rw [deriv_Jcost_eq x hx]
  85  unfold linJ
  86  -- Key algebraic step: (1 - x⁻²) * x = x - x⁻¹
  87  have h_key : (1 - x⁻¹ ^ 2) * x = x - x⁻¹ := by
  88    have h1 : x⁻¹ ^ 2 * x = x⁻¹ := by
  89      rw [pow_two]
  90      calc x⁻¹ * x⁻¹ * x = x⁻¹ * (x⁻¹ * x) := by ring
  91        _ = x⁻¹ * 1 := by rw [inv_mul_cancel₀ hxne]
  92        _ = x⁻¹ := by ring
  93    calc (1 - x⁻¹ ^ 2) * x
  94        = x - x⁻¹ ^ 2 * x := by ring
  95      _ = x - x⁻¹ := by rw [h1]
  96  calc ((x - x⁻¹) / 2) * L
  97      = (x - x⁻¹) / 2 * L := by ring
  98    _ = ((1 - x⁻¹ ^ 2) * x) / 2 * L := by rw [h_key]
  99    _ = (1 - x⁻¹ ^ 2) / 2 * x * L := by ring
 100
 101/-! ## Remainder Bound -/
 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
 136    linJ x L = deriv Jcost x * x * L :=
 137  linJ_eq_derivative_times_x x L hx
 138
 139end Cost
 140end IndisputableMonolith
 141