defectDist_le_J_of_ratio_bounds
plain-language theorem explainer
Pairs of positive reals with ratio in the closed interval [1/M, M] obey defectDist x y ≤ J M. Workers deriving local cost bounds from the Recognition Composition Law cite the result when assembling quasi-triangle estimates. The argument is a one-line wrapper that unfolds the defect definition and invokes the endpoint bound on J.
Claim. Let $M ≥ 1$, $x > 0$, $y > 0$. If $1/M ≤ x/y ≤ M$, then $J(x/y) ≤ J(M)$, where $J(r) = ½(r + r^{-1}) - 1$.
background
J is the canonical cost function satisfying the Recognition Composition Law, given explicitly by J(r) = ½(r + r^{-1}) - 1. Defect distance is the derived quantity defectDist x y := J(x/y), which vanishes at equality and is symmetric and nonnegative. The module works inside the algebra generated by this cost on positive reals. The key upstream lemma J_le_J_of_inv_le_le states that J(r) ≤ J(M) whenever r lies in [1/M, M] and M ≥ 1; the present theorem simply rewrites that statement in defect-distance language.
proof idea
one-line wrapper that unfolds defectDist and applies J_le_J_of_inv_le_le
why it matters
The bound is the immediate prerequisite for defectDist_quasi_triangle_local (the local form of Proposition 2.6), which inserts the factor (M + 2 + M^{-1})/2 into the quasi-triangle inequality under the same ratio control. It therefore supplies the concrete constant K_M that appears in the Recognition framework when edge ratios are bounded by the eight-tick octave parameter M.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.