defectDist_quasi_triangle_local
plain-language theorem explainer
Researchers studying metric properties of the J-cost function in Recognition Science would cite this local quasi-triangle inequality for the defect distance. When ratios x/y and y/z lie between 1/M and M for M ≥ 1, defect distance d(x,z) satisfies d(x,z) ≤ K_M (d(x,y) + d(y,z)) with K_M = (M + 2 + M^{-1})/2. The proof reduces the claim to submultiplicativity of J on the product of ratios, bounds the quadratic cross term via individual defects at most J(M), and closes by algebraic simplification using the explicit constant identity.
Claim. Let $d(x,y) := J(x/y)$ denote the defect distance. For $M ≥ 1$ and positive reals $x,y,z$ satisfying $1/M ≤ x/y ≤ M$ and $1/M ≤ y/z ≤ M$, it holds that $d(x,z) ≤ ((M + 2 + M^{-1})/2) (d(x,y) + d(y,z))$.
background
The defect distance is defined by defectDist x y := J(x/y), where J(t) = (t + t^{-1})/2 - 1 satisfies the Recognition Composition Law. This local result assumes ratios bounded by M, which permits bounding each defectDist by J(M) via the lemma defectDist_le_J_of_ratio_bounds. It builds directly on Jcost_submult for the submultiplicative inequality J((x/y)(y/z)) ≤ 2J(x/y) + 2J(y/z) + 2J(x/y)J(y/z) and on defectDist_nonneg for non-negativity of each term. The setting is the CostAlgebra module, part of establishing quasi-triangle bounds as in Proposition 2.6.
proof idea
The proof first records positivity of M and the ratios, then uses the identity (x/y)(y/z) = x/z. It applies Jcost_submult to obtain defectDist x z ≤ 2 defectDist x y + 2 defectDist y z + 2 defectDist x y defectDist y z. It invokes defectDist_le_J_of_ratio_bounds to bound each defect by J(M), records non-negativity, and proves the cross-term inequality 2 dxy dyz ≤ JM (dxy + dyz) by splitting into two multiplications followed by nlinarith. A final calc block rewrites the right-hand side to (2 + JM) times the sum of defects, which equals the target constant by quasiTriangleConstant_eq.
why it matters
This theorem supplies the local form of Proposition 2.6 on quasi-triangle bounds for the defect distance. It serves as a building block in the algebra of costs, supporting metric-like inequalities under bounded ratios that arise from the J-uniqueness and Recognition Composition Law in the forcing chain. The constant K_M is derived from the explicit form of J. No immediate downstream uses appear in the module graph, but the result closes a key step in §5a of the CostAlgebra development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.