Cost Derivative Differentiable At Jcost

Smoothness of the cost curve

The J-cost function is defined as J(x) = (x + 1/x)/2 - 1, a formula that measures the price of a recognition event when the input is x. The declaration differentiableAt_Jcost establishes that this function has a derivative at every positive real number x. In plain terms, the cost curve is smooth: it has no corners, jumps, or breaks anywhere on the positive half-line. The proof is routine calculus, building the derivative from the sum, reciprocal, and constant terms that make up J.

The derivative itself is J'(x) = (1 - 1/x²)/2, also proved in the same module. This formula shows how the cost changes per unit change in x. At x = 1, the derivative is zero, meaning the cost is locally flat at the unit multiplier. For x > 1, the derivative is positive, so cost rises as x grows; for 0 < x < 1, the derivative is negative, so cost falls as x approaches 1 from below. This matches the known minimum of J at x = 1, where J(1) = 0.

The derivative enables a linear approximation: for a small multiplicative change L, the change in cost is approximately J'(x) · x · L. The module proves this linear term equals ((x - 1/x)/2) · L, and that the remainder after this linearization is quadratic in L. This is the standard Taylor expansion idea: the first-order term captures the dominant behavior, and the error shrinks like L² for small L.

In Recognition Science, this smoothness result is what allows the framework to replace an axiom about harm with a derived linear bound. The module states that the linearized bond delta, which measures first-order harm from a log-strain L at base x, is exactly the directional derivative of J along the exponential path. This means the harm term is not an additional assumption but a consequence of the cost function's shape. The framework's library, a machine-checked collection of formal theorems, records this as a proved theorem.

What the declaration does not claim is just as important. It does not assert that J is differentiable at x = 0 or at negative x; the proof requires x > 0, and the formula has a singularity at zero. It does not claim that the linear approximation is exact; the remainder term is generally nonzero, only quadratically small. And it does not by itself establish the uniqueness of J, which is a separate theorem about the functional equation. The derivative result is a local smoothness fact, not a global characterization of the cost function.

/-- J(x) = (x + x⁻¹)/2 - 1 is differentiable for x > 0. -/
lemma differentiableAt_Jcost (x : ℝ) (hx : 0 < x) : DifferentiableAt ℝ Jcost x := by
  have hxne : x ≠ 0 := ne_of_gt hx
  unfold Jcost
  apply DifferentiableAt.sub
  · apply DifferentiableAt.div_const
    apply DifferentiableAt.add differentiableAt_id
    exact differentiableAt_inv hxne
  · exact differentiableAt_const 1

/-- 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

/-- **Main Theorem**: The harm linear term is the correct directional derivative.

    This justifies using linBondDelta in the harm decomposition. -/
theorem harm_linearization_correct (x L : ℝ) (hx : 0 < x) :
    -- The linearization linJ captures the first-order behavior of J along exp paths
    linJ x L = deriv Jcost x * x * L :=
  linJ_eq_derivative_times_x x L hx

What this page does not claim

The declaration does not prove differentiability at x = 0 or for negative x. The linear approximation is not exact; the remainder term is nonzero in general. The derivative result does not by itself establish the uniqueness of the J-cost function.

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: