defectDist
plain-language theorem explainer
The defect distance is defined as d(x, y) = J(x/y) for positive reals x and y, where J is the unique cost function satisfying the Recognition Composition Law. Researchers developing algebraic properties of costs in the Recognition Science framework cite this as the basic deviation measure. The definition is a direct abbreviation substituting the ratio into the explicit J expression.
Claim. The defect distance between positive real numbers $x$ and $y$ is defined by $d(x,y) := J(x/y)$, where the J-cost function is $J(z) = (1/2)(z + z^{-1}) - 1$.
background
In the CostAlgebra module the J-cost function is the unique map satisfying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and taking the closed form J(z) = ½(z + z^{-1}) - 1. The defect distance is obtained simply by feeding the ratio x/y into this cost. The module sits after imports from Cost, FunctionalEquation and FunctionalEquationAczel, placing the construction inside the algebraic development that follows the forcing chain T0-T8.
proof idea
This is a direct definition that applies the J-cost function to the ratio of the two arguments.
why it matters
The definition supplies the core object for the six downstream results in the same module, including defectDist_nonneg, defectDist_symm, defectDist_self, defectDist_quasi_triangle_local and defectDist_no_global_quasi_triangle. It supplies the algebraic substrate for cost-based deviation measures that connect to J-uniqueness (T5) and the self-similar fixed point phi (T6). It leaves open the question of whether a global quasi-triangle inequality can be recovered under weaker ratio bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.