Cost Derivative Deriv Jcost Eq

The derivative of cost

The cost function J(x) = (x + 1/x)/2 - 1 measures how far a multiplier x pushes a quantity away from its balanced value of 1. For example, J(2) = (2 + 1/2)/2 - 1 = 0.25, while J(1) = 0. The derivative of this function, written J'(x), tells how steeply the cost rises when x moves slightly. The declaration deriv_Jcost_eq establishes that for any positive x, J'(x) = (1 - 1/x²)/2. This is a pure calculus fact: differentiate (x + 1/x)/2 - 1 term by term, get (1 - 1/x²)/2, and the constant -1 vanishes.

The derivative is zero exactly at x = 1, where the cost is already at its minimum of zero. For x greater than 1, the derivative is positive, meaning cost increases as x grows. For x between 0 and 1, the derivative is negative, meaning cost decreases as x approaches 1 from below. This matches the symmetry J(1/x) = J(x): the cost treats doubling and halving identically, and the derivative flips sign under the reciprocal map.

In Recognition Science, this derivative becomes the backbone of a linear approximation. The framework defines a linearized bond delta linJ(x, L) = ((x - 1/x)/2) · L, where L is a small logarithmic strain. The theorem linJ_eq_derivative_times_x proves that linJ(x, L) = J'(x) · x · L for x > 0. In plain words: the first-order change in cost under a small multiplicative perturbation equals the derivative times the current scale x times the strain L. The remainder after this linear term is quadratic in L, so the approximation is accurate for small L.

The declaration does not claim that the derivative formula itself is new mathematics; it is a standard calculus result, machine-checked in the framework's library of formal theorems. Nor does it claim that the linear approximation is exact for large strains; the remainder term grows quadratically. It also does not claim that the derivative formula forces the full cost function; the uniqueness of J comes from separate functional-equation axioms, not from this derivative identity.

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

/-- The key identity connecting linJ to the derivative:
    linJ(x, L) = J'(x) · x · L

    Algebraic identity: (x - x⁻¹)/2 = ((1 - x⁻²)/2) · x -/
theorem linJ_eq_derivative_times_x (x L : ℝ) (hx : 0 < x) :
    linJ x L = deriv Jcost x * x * L := by
  have hxne : x ≠ 0 := ne_of_gt hx
  rw [deriv_Jcost_eq x hx]
  unfold linJ
  -- Key algebraic step: (1 - x⁻²) * x = x - x⁻¹
  have h_key : (1 - x⁻¹ ^ 2) * x = x - x⁻¹ := by
    have h1 : x⁻¹ ^ 2 * x = x⁻¹ := by
      rw [pow_two]
      calc x⁻¹ * x⁻¹ * x = x⁻¹ * (x⁻¹ * x) := by ring
        _ = x⁻¹ * 1 := by rw [inv_mul_cancel₀ hxne]
        _ = x⁻¹ := by ring
    calc (1 - x⁻¹ ^ 2) * x
        = x - x⁻¹ ^ 2 * x := by ring
      _ = x - x⁻¹ := by rw [h1]
  calc ((x - x⁻¹) / 2) * L
      = (x - x⁻¹) / 2 * L := by ring
    _ = ((1 - x⁻¹ ^ 2) * x) / 2 * L := by rw [h_key]
    _ = (1 - x⁻¹ ^ 2) / 2 * x * L := by ring

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

What this page does not claim

The derivative formula is new mathematics; it is a standard calculus result. The linear approximation is exact for large strains; the remainder grows quadratically. The derivative identity alone forces the cost function; uniqueness comes from separate functional-equation axioms.

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: