defectDist_nonneg
plain-language theorem explainer
Defect distance d(x,y) = J(x/y) is non-negative for all positive reals x and y. Recognition Science algebraists cite this to confirm defectDist forms a non-negative cost measure. The proof is a one-line term application of J_nonneg to the positive ratio x/y.
Claim. For positive real numbers $x>0$ and $y>0$, the defect distance satisfies $0 ≤ J(x/y)$, where $J$ is the recognition cost function.
background
In the CostAlgebra module the defect distance is defined by defectDist x y := J (x / y). It quantifies the cost of deviation between two positive reals, satisfying d(x,x)=0 by direct substitution and symmetry via J reciprocity. The module imports Cost, FunctionalEquation and FunctionalEquationAczel, locating the result inside the algebraic development of the J-cost induced by multiplicative recognizers. Upstream, J_nonneg supplies the non-negativity of J(z) for z>0, while ObserverForcing.cost records that every recognition event carries non-negative J-cost.
proof idea
One-line term proof that applies J_nonneg directly to the ratio x/y, justified by the positivity of division under the hypotheses hx and hy.
why it matters
Non-negativity of defectDist is required by the downstream local quasi-triangle theorem defectDist_quasi_triangle_local (Proposition 2.6), which bounds defectDist x z by a multiple of the sum of adjacent defects on bounded ratios. The result therefore anchors the interpretation of defect distance as a non-negative cost in the Recognition framework, consistent with J-uniqueness (T5) and the forcing chain that derives the cost function from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.