Cost Derivative Lin J Matches Harm Def

The linearized bond delta

The cost function J(x) = (x + 1/x)/2 - 1 measures how far a multiplier x is from 1. It is zero at x=1 and grows as x moves away, whether by increase or decrease. Its derivative, J'(x) = (1 - 1/x²)/2, tells how steeply the cost changes at a given x. The identity linJ_matches_harm_def states that the linearized bond delta, defined as ((x - 1/x)/2) · L, is exactly this derivative multiplied by x and by the log-strain L. In plain terms: the linear term used in harm calculations is precisely the first-order Taylor approximation of the cost along an exponential path.

This is a formal theorem in the framework's machine-checked library of formal theorems, proved by unfolding definitions and simplifying. It does not introduce new physics. It does not say that the linear term equals the full cost, nor that higher-order terms vanish. It only establishes that the linearization is the correct directional derivative, a standard calculus fact. The remainder after linearization, remJ(x, L) = J(x·e^L) - J(x) - linJ(x, L), is separately defined and is O(L²), meaning it shrinks quadratically as L goes to zero.

The theorem's role is architectural, not empirical. It connects the cost derivative theory to the Ethics/Harm module, where linBondDelta appears. By proving linJ_matches_harm_def, the library shows that the harm linear term is not an arbitrary choice but the first-order approximation of the J-cost. This justifies using it in harm decompositions. The theorem does not claim that harm is fully captured by this linear term, nor that the cost function itself is derived from harm considerations. It is a bridge between two formal definitions, ensuring consistency within the framework.

What the declaration does not claim is equally important. It does not assert that the linearized bond delta is a measured quantity or a physical law. It does not claim that the remainder is zero; the remainder is nonzero for finite L. It does not claim that the derivative formula holds at x=0, where J is not differentiable. The theorem is conditional on x > 0, as are the derivative lemmas. Finally, it does not claim that the cost function J is the only possible cost function; that uniqueness is a separate theorem about the functional equation, not about this derivative identity.

/-- Matches the linBondDelta definition in Harm.lean. -/
theorem linJ_matches_harm_def (x L : ℝ) :
    linJ x L = ((x - x⁻¹) / 2) * L := rfl

/-- The remainder term after linearization:
    rem(x, L) = J(x·e^L) - J(x) - linJ(x, L) -/
noncomputable def remJ (x L : ℝ) : ℝ :=
  Jcost (x * exp L) - Jcost x - linJ x L

-- TODO: Quadratic Remainder Bound
-- theorem remJ_quadratic_bound (x : ℝ) (hx : 0 < x) :
--     ∃ C > 0, ∀ L, |L| ≤ 1 → |remJ x L| ≤ C * L ^ 2

/-- The derivative of J at x equals (1 - x⁻²)/2.

    Proof: J(x) = (x + x⁻¹)/2 - 1
    J'(x) = d/dx[(x + x⁻¹)/2 - 1] = (1 + (-x⁻²))/2 = (1 - x⁻²)/2

    **Technical note**: This is standard calculus, using:
    - d/dx[x] = 1
    - d/dx[x⁻¹] = -x⁻² -/
lemma deriv_Jcost_eq (x : ℝ) (hx : 0 < x) :
    deriv Jcost x = (1 - x⁻¹ ^ 2) / 2 := by
  have hxne : x ≠ 0 := ne_of_gt hx
  -- J(x) = (x + x⁻¹)/2 - 1
  -- J'(x) = (1 + d/dx[x⁻¹])/2 = (1 - x⁻²)/2
  -- Use HasDerivAt to compute the derivative
  have h_inv : HasDerivAt (·⁻¹) (-(x ^ 2)⁻¹) x := hasDerivAt_inv hxne
  have h_id : HasDerivAt id 1 x := hasDerivAt_id x
  have h_add : HasDerivAt (fun y => y + y⁻¹) (1 + -(x ^ 2)⁻¹) x :=
    h_id.add h_inv
  have h_div : HasDerivAt (fun y => (y + y⁻¹) / 2) ((1 + -(x ^ 2)⁻¹) / 2) x :=
    h_add.div_const 2
  have h_sub : HasDerivAt (fun y => (y + y⁻¹) / 2 - 1) ((1 + -(x ^ 2)⁻¹) / 2) x :=
    h_div.sub_const 1
  -- h_sub gives: HasDerivAt Jcost ((1 - x⁻²) / 2) x
  have h_eq : (1 + -(x ^ 2)⁻¹) / 2 = (1 - x⁻¹ ^ 2) / 2 := by
    have h1 : (x ^ 2)⁻¹ = x⁻¹ ^ 2 := by
      rw [pow_two, pow_two, mul_inv_rev]
    rw [h1]
    ring
  rw [h_eq] at h_sub
  exact h_sub.deriv

What this page does not claim

The linear term equals the full cost for finite L; the remainder is nonzero. The cost function J is the only possible cost function; uniqueness is a separate theorem. The derivative formula holds at x=0, where J is not differentiable.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/Derivative.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: