defectDist_no_global_quasi_triangle
plain-language theorem explainer
No finite constant K greater than one can serve as a quasi-triangle factor for the defect distance on all positive real triples. Algebraists studying metric properties of the J-cost in Recognition Science cite this when ruling out uniform control on deviation costs. The proof assumes such a K exists, specializes to the geometric triple 1, r, r squared with r set to twice K, applies the Recognition Composition Law to express J of r squared in terms of J of r, and derives contradictory upper and lower bounds on K.
Claim. There does not exist a real number $K > 1$ such that for all positive reals $x, y, z$ one has $d(x, z) ≤ K · (d(x, y) + d(y, z))$, where $d(a, b) := J(a/b)$ and $J$ obeys the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$.
background
Defect distance is defined by defectDist x y = J(x/y). It measures the cost of deviation between positive reals, vanishes at equality, is symmetric by J reciprocity, and is nonnegative. The Recognition Composition Law is the identity J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), described in upstream results as the foundational identity from which everything else follows. J itself is normalized so that J(1) = 0 and satisfies J(x) = J(1/x) for x > 0.
proof idea
Assume for contradiction that a K > 1 exists with the global quasi-triangle property. Set r := 2K. Apply the assumed inequality to the triple 1, r, r². Use J_reciprocal to obtain defectDist(1, r) = J r and defectDist(r, r²) = J r. Use RCL_holds on r and r together with J_at_one to derive J(r²) = 2(J r)² + 4 J r. Substitute into the inequality to reach 2(J r)² + 4 J r ≤ K · 2 J r. Invoke J_nonneg and Jcost_eq_zero_iff to confirm J r > 0, simplify to J r + 2 ≤ K, then use the explicit form of J r at this r to obtain the reverse strict inequality K < J r + 2 and reach a contradiction by linarith.
why it matters
This is the global form of Proposition 2.6. It shows that the defect distance induced by the J-cost cannot be bounded by any uniform quasi-triangle factor across all positive scales, even though the underlying Recognition Composition Law holds. The result closes an avenue for treating defectDist as a global metric and supports the framework's focus on discrete structures such as the phi-ladder and eight-tick octave rather than continuous metric completions. No downstream citations appear in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.