jcost_gradient_descent_converges
plain-language theorem explainer
Gradient descent on the J-cost function J(x) = (x + x^{-1})/2 - 1 moves any positive x ≠ 1 strictly closer to the unique minimum at x = 1 when the step size η is positive. Complexity theorists analyzing the tractability of physical ground-state search would invoke this result to establish that local J-cost minimization is efficient. The proof proceeds by case analysis on whether x exceeds or falls below 1, invokes the sign of the derivative from adjacent lemmas, and closes with linear arithmetic.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. For any $x > 0$ with $x ≠ 1$ and any step size η > 0, the updated value satisfies $x - η J'(x) < x$ whenever $x > 1$, and $x - η J'(x) > x$ whenever $x < 1$.
background
The module Information.PhysicsComplexityStructure frames the computational complexity of physics via J-cost minimization. J-cost is the cost function J(x) = (x + x^{-1})/2 - 1 induced by multiplicative recognizers (from MultiplicativeRecognizerL4.cost) and recognition events (from ObserverForcing.cost). The module states that J-cost is strictly convex with unique global minimum at x = 1, verifiable in O(1) time, and that gradient descent converges monotonically to this ground state.
proof idea
The term-mode proof constructs the conjunction of the two implications. For the x > 1 branch it applies jcost_deriv_pos_of_gt_one to obtain a positive derivative and closes with linarith using positivity of η. For the x < 1 branch it applies jcost_deriv_neg_of_lt_one, forms the negative product via mul_neg_of_pos_of_neg, and again closes with linarith.
why it matters
Labeled IC-005.16, the theorem supports the module's complexity summary that lists J-cost gradient descent as converging monotonically and places ground-state verification in P. It rests on J-uniqueness from the forcing chain (T5) and the Recognition Composition Law. The result feeds the claim that local 8-tick dynamics remain O(1) per step while φ-rung computations remain EXPTIME.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.