Information Physics Complexity Structure Jcost Deriv Pos Of Gt One

The slope of the cost function

In Recognition Science, the ledger, a discrete record of events, assigns a cost to every possible state of a system. The cost function is J(x) = (x + 1/x)/2 - 1, which is strictly convex and has its unique global minimum at x = 1. The declaration jcost_deriv_pos_of_gt_one establishes a simple fact about the slope of this function: for any positive input x greater than 1, the derivative of J at x is strictly positive. In plain terms, if a state is above the balanced value, increasing that value further raises the cost, so a search for the minimum naturally pushes it downward.

This theorem is one half of a pair. Its counterpart, jcost_deriv_neg_of_lt_one, states that for any positive x less than 1, the derivative is strictly negative. Together they show that the cost function slopes upward on both sides of its minimum at x = 1. The two results combine in the theorem jcost_gradient_descent_converges, which proves that a simple gradient descent step, subtracting a positive multiple of the derivative from the current value, always moves a state closer to 1: values above 1 decrease, values below 1 increase. This holds for any positive step size, so the convergence is monotonic and unconditional within the positive domain.

The theorem does not claim that the gradient descent reaches the minimum in finite time, nor does it bound the number of steps required. It also does not assert that the cost function is globally convex over all real numbers; the domain is restricted to positive inputs, and the derivative is defined only there. The result is local in the sense that it describes the slope at a single point, not the behavior of the function over an interval. It says nothing about the computational complexity of finding the minimum, only that a particular iterative method will make progress toward it.

Within the framework, this slope fact underpins the claim that J-cost minimization is computationally tractable. The library's complexity summary lists ground state verification as linear in system size, and J-cost gradient descent as converging monotonically to x = 1. The theorem jcost_deriv_pos_of_gt_one is the analytic engine behind that convergence claim: it guarantees that the descent direction is always correct when the current state is above the optimum. Without this sign guarantee, a gradient method could overshoot or wander; with it, the path to the minimum is assured.

/-- **THEOREM IC-005.7**: J'(x) > 0 for x > 1.
    The gradient points upward away from the minimum for x > 1. -/
theorem jcost_deriv_pos_of_gt_one (x : ℝ) (hx : x > 1) :
    jcost_deriv x > 0 := by
  unfold jcost_deriv
  apply div_pos _ (by norm_num)
  have hxpos : (0 : ℝ) < x := by linarith
  have hxinv_lt1 : x⁻¹ < 1 := by
    rw [inv_eq_one_div, div_lt_one (by linarith : (0:ℝ) < x)]; linarith
  have hxinv_pos : (0 : ℝ) < x⁻¹ := inv_pos.mpr hxpos
  have : 1 - (x⁻¹)^2 > 0 := by
    have h4 : (1 - x⁻¹) * (1 + x⁻¹) = 1 - (x⁻¹)^2 := by ring
    rw [← h4]
    exact mul_pos (by linarith) (by linarith)
  linarith

/-- **THEOREM IC-005.8**: J'(x) < 0 for 0 < x < 1.
    The gradient points downward, pushing toward the minimum for x < 1. -/
theorem jcost_deriv_neg_of_lt_one (x : ℝ) (hx : x > 0) (hlt : x < 1) :
    jcost_deriv x < 0 := by
  unfold jcost_deriv
  apply div_neg_of_neg_of_pos _ (by norm_num)
  have : (x⁻¹)^2 > 1 := by
    apply one_lt_pow₀ _ (by norm_num)
    exact one_lt_inv_iff₀.mpr ⟨hx, hlt⟩
  linarith

/-- **THEOREM IC-005.16**: Gradient descent on J-cost converges toward x = 1.
    For x > 1: one gradient step x₁ = x₀ - η J'(x₀) moves closer to x = 1.
    This makes J-cost minimization efficiently solvable. -/
theorem jcost_gradient_descent_converges (x : ℝ) (hx_pos : x > 0) (hx_ne : x ≠ 1)
    (η : ℝ) (hη_pos : η > 0) :
    (x > 1 → x - η * jcost_deriv x < x) ∧
    (x < 1 → x - η * jcost_deriv x > x) := by
  constructor
  · intro h
    have hd : jcost_deriv x > 0 := jcost_deriv_pos_of_gt_one x h
    linarith [mul_pos hη_pos hd]
  · intro h
    have hd : jcost_deriv x < 0 := jcost_deriv_neg_of_lt_one x hx_pos h
    have : η * jcost_deriv x < 0 := mul_neg_of_pos_of_neg hη_pos hd
    linarith

What this page does not claim

The theorem does not bound the number of gradient descent steps required for convergence. The derivative is not defined for non-positive inputs, and the theorem says nothing about such values. The result does not imply that the global minimum is reachable in polynomial time, only that descent moves toward it.

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/Information/PhysicsComplexityStructure.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: