add_inv_mono_on_one
plain-language theorem explainer
The lemma establishes that x + x^{-1} is non-decreasing for real x, y with 1 ≤ x ≤ y. Researchers analyzing continued-fraction convergence to φ or J-cost growth along the phi-ladder cite this algebraic fact. The proof factors the difference (y + y^{-1}) - (x + x^{-1}) as (y - x)(1 - 1/(x y)), then verifies both factors are nonnegative via positivity of x, y and the product x y ≥ 1.
Claim. For all real numbers $x, y$ with $1 ≤ x ≤ y$, the inequality $x + x^{-1} ≤ y + y^{-1}$ holds.
background
The ContinuedFractionPhi module interprets continued fractions as sequential J-cost minimizers, where J(x) = ½(x + x^{-1}) - 1 attains its global minimum at x = 1 and has self-similar fixed point φ. The present lemma supplies the monotonicity of the sum term x + x^{-1} on [1, ∞), which is the direct algebraic prerequisite for the companion statement that Jcost itself is monotone on the same interval.
proof idea
The tactic proof first obtains 0 < x and 0 < y from 1 ≤ x. It derives 1 ≤ x y by nlinarith. The difference is rewritten by field_simp and ring as (y - x)(1 - 1/(x y)). Non-negativity of y - x is immediate; the second factor is recast as (x y - 1)/(x y) and shown nonnegative by division of nonnegative terms. Multiplication yields a nonnegative difference, and linarith finishes the proof.
why it matters
The result is invoked by Jcost_mono_on_one (both in ContinuedFractionPhi and in PhiLadderStability), which in turn supports stability of the phi-ladder. It supplies the missing monotonicity step in the Recognition Science argument that continued fractions converge to φ because J-cost is strictly convex and φ is the unique attractor of the recursion x ↦ 1 + 1/x (T5 J-uniqueness). The lemma is fully discharged with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.