defectDist_le_J_of_ratio_bounds
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not claim the inequality when the ratio x/y lies outside [1/M, M].
- Does not produce a global triangle inequality without an a-priori M bound.
- Does not apply when x or y is non-positive.
- Does not evaluate the numerical size of J(M) beyond the closed-form definition.
Lean usage
have hxy : defectDist x y <= J M := defectDist_le_J_of_ratio_bounds hM hx hy hxy_lower hxy_upperformal statement (Lean)
361theorem defectDist_le_J_of_ratio_bounds {M x y : ℝ} (hM : 1 ≤ M)
362 (hx : 0 < x) (hy : 0 < y)
363 (hxy_lower : 1 / M ≤ x / y) (hxy_upper : x / y ≤ M) :
364 defectDist x y ≤ J M := by
proof body
Term-mode proof.
365 unfold defectDist
366 exact J_le_J_of_inv_le_le hM (div_pos hx hy) hxy_lower hxy_upper
367
368/-- The local quasi-triangle constant from Proposition 2.6. -/