defectDist_le_J_of_ratio_bounds
plain-language theorem explainer
Pairs of positive reals x and y whose ratio lies in the symmetric interval [1/M, M] for M >= 1 satisfy defectDist x y <= J(M). Researchers establishing local quasi-triangle inequalities for the J-cost in Recognition Science would cite this bound when controlling deviation costs on bounded ratios. The proof is a one-line wrapper that unfolds defectDist to J(x/y) and invokes the endpoint-maximum theorem J_le_J_of_inv_le_le on the given ratio bounds.
Claim. Let $M >= 1$, $x > 0$, $y > 0$. If $1/M <= x/y <= M$, then $J(x/y) <= J(M)$, where $J(r) = 1/2 (r + r^{-1}) - 1$ and $J$ is the unique cost satisfying the Recognition Composition Law.
background
The J-cost is the function J(x) = 1/2 (x + x^{-1}) - 1, the unique cost satisfying the Recognition Composition Law RCL. The defect distance is defined by defectDist x y := J(x/y); it vanishes at x = y, is symmetric, and is nonnegative. The upstream lemma J_le_J_of_inv_le_le states that on the interval [1/M, M] the function J attains its maximum at the endpoints, so J(r) <= J(M) whenever 1/M <= r <= M and r > 0.
proof idea
The proof is a term-mode one-liner: unfold defectDist to replace the left-hand side by J(x/y), then apply J_le_J_of_inv_le_le directly to the hypotheses 1 <= M, 0 < x/y, 1/M <= x/y and x/y <= M.
why it matters
This bound is the immediate prerequisite for the local quasi-triangle inequality defectDist_quasi_triangle_local (Proposition 2.6), which supplies the constant K_M = (M + 2 + M^{-1})/2 used in bounded-ratio estimates throughout the cost algebra. It therefore supports the algebraic infrastructure that later yields the phi-ladder mass formula and the eight-tick octave in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.