Jcost_mono_on_one
plain-language theorem explainer
The J-cost function increases monotonically for arguments at least 1. Analysts studying the stability of the golden-ratio ladder or the minimal cost of continued-fraction partial quotients cite this result to bound excitation energies. The proof reduces the claim to the already-established monotonicity of x + x inverse on the same interval and concludes by linear arithmetic.
Claim. For all real numbers $x$ and $y$ satisfying $1 ≤ x ≤ y$, one has $J(x) ≤ J(y)$, where $J(z) = ½(z + z^{-1}) - 1$.
background
The J-cost functional is defined by $J(z) = ½(z + z^{-1}) - 1$. It attains its global minimum of zero at $z = 1$ and is strictly convex on the positive reals. The present lemma establishes that J is increasing on the ray [1, ∞). This module develops the continued-fraction representation of φ as the fixed point of the recursion $x = 1 + 1/x$, which arises as the ground-state geodesic under sequential J-cost minimization. The upstream lemma add_inv_mono_on_one supplies the monotonicity of the auxiliary map $z ↦ z + z^{-1}$ on [1, ∞).
proof idea
The proof is a one-line wrapper. It unfolds the definition of Jcost, invokes the monotonicity of $x + x^{-1}$ on [1, ∞) supplied by add_inv_mono_on_one, and finishes with linear arithmetic.
why it matters
This monotonicity result is invoked by the theorem establishing that the partial quotient 1 (corresponding to the ratio φ) achieves minimal J-cost among positive integers, and by the statements that gap costs and first-excited costs grow monotonically on the φ-ladder. It therefore closes the argument that φ is the unique attractor of the continued-fraction recursion and supplies the ordering needed for the phi-ladder stability theorems. The result rests on the convexity properties of J derived from the Recognition Science forcing chain at step T5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.