defectDist_nonneg
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply when x or y is zero or negative.
- Does not establish the triangle inequality.
- Does not quantify the distance in terms of other parameters.
- Does not address equality cases beyond d(x,x)=0.
formal statement (Lean)
328theorem defectDist_nonneg (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
329 0 ≤ defectDist x y :=
proof body
Term-mode proof.
330 J_nonneg (x / y) (div_pos hx hy)
331
332/-! ## §5a. Quasi-Triangle Bounds for the Defect Distance -/
333
334/-- On the symmetric interval `[1 / M, M]`, the canonical cost is bounded by
335 its endpoint value `J(M)`. -/