defectDist
plain-language theorem explainer
defectDist introduces the defect distance d(x,y) = J(x/y) on the reals, with J the unique cost obeying the Recognition Composition Law. Cost-algebra researchers cite it when deriving metric properties from the J function. The definition is a direct abbreviation that feeds the non-negativity, symmetry, and local quasi-triangle results proved immediately downstream.
Claim. The defect distance between reals $x$ and $y$ is $d(x,y) := J(x/y)$, where $J(z) = (z + z^{-1})/2 - 1$.
background
In CostAlgebra the J-cost is the function J(z) = (z + z^{-1})/2 - 1 that satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The defect distance is obtained simply by feeding the ratio x/y into this J. The module imports the base Cost and FunctionalEquation files that establish J-uniqueness and the identity event at which J vanishes.
proof idea
Direct definition that applies the sibling J to the ratio of the two arguments.
why it matters
defectDist supplies the concrete distance used by defectDist_nonneg, defectDist_symm, defectDist_self and the local quasi-triangle theorem defectDist_quasi_triangle_local. It translates the T5 J-uniqueness and the Recognition Composition Law into a deviation measure that supports the eight-tick octave and D=3 geometry downstream. No open scaffolding is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.