J_le_J_of_inv_le_le
plain-language theorem explainer
J(r) ≤ J(M) holds for M ≥ 1 and r in the closed interval [1/M, M]. Cost-algebra workers cite the bound when controlling defects for ratio-constrained pairs. The argument factors the difference (M + M^{-1}) - (r + r^{-1}) to establish nonnegativity of the numerator under the given bounds, then applies linear arithmetic after unfolding the definition of J.
Claim. Let $M ≥ 1$ and $r > 0$ satisfy $1/M ≤ r ≤ M$. Then $J(r) ≤ J(M)$, where $J(x) := ½(x + x^{-1}) - 1$.
background
The J-cost is the unique function satisfying the Recognition Composition Law, given explicitly by J(x) = ½(x + x^{-1}) - 1. The defect functional equals J on positive reals. This theorem lives in the CostAlgebra module, which assembles inequalities for the canonical cost under the RecognitionStructure M imported from Recognition and Cycle3.
proof idea
The tactic proof first obtains positivity of M. It factors M + M^{-1} - (r + r^{-1}) as ((M - r)(Mr - 1))/(Mr) and shows the numerator is nonnegative from the interval hypotheses. The positive denominator then yields r + r^{-1} ≤ M + M^{-1}, from which the J inequality follows by definition and linarith.
why it matters
The result supplies the core inequality used by defectDist_le_J_of_ratio_bounds to bound defectDist(x, y) whenever the ratio x/y lies in [1/M, M]. It advances the cost-composition development in the algebra and aligns with J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.