quasiTriangleConstant_eq
plain-language theorem explainer
The equality identifies the quasi-triangle constant K_M as 2 + J(M), which simplifies to (M + 2 + M^{-1})/2. Researchers working on bounded-ratio defect distances in Recognition Science cite it to instantiate the constant inside the local form of Proposition 2.6. The proof is a direct algebraic reduction after unfolding the definition of J.
Claim. For any real number $M$, $2 + J(M) = (M + 2 + M^{-1})/2$, where $J(x) = (1/2)(x + x^{-1}) - 1$ is the J-cost function.
background
The J-cost function is the unique cost satisfying the Recognition Composition Law, given explicitly by J(x) = ½(x + x⁻¹) − 1. The defect functional equals J for positive arguments. This theorem sits in the CostAlgebra module, which assembles algebraic identities for costs derived from the Recognition framework and its functional equations.
proof idea
The proof is a one-line wrapper that unfolds J and Jcost then applies the ring tactic to confirm the algebraic identity.
why it matters
This declaration supplies the explicit value of the constant K_M used in the local quasi-triangle inequality defectDist_quasi_triangle_local, the local form of Proposition 2.6. It connects the constant directly to the J-cost arising from the Recognition Composition Law. The result supports the quasi-triangle bound on bounded edge-ratios within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.