defectDist
Defect distance d(x, y) is defined by applying the J-cost function to the ratio x/y for positive reals x and y. Researchers working on Recognition Science algebra cite it when establishing metric-like properties such as non-negativity and symmetry on ratios. The definition is a one-line wrapper that substitutes the ratio directly into J.
claimThe defect distance between positive real numbers $x$ and $y$ is $d(x,y) := J(x/y)$, where $J(z) = ½(z + z^{-1}) - 1$.
background
The J-cost function is the unique cost satisfying the Recognition Composition Law, given explicitly by $J(x) = ½(x + x^{-1}) - 1$. In the CostAlgebra module, defectDist supplies the deviation measure obtained by feeding the ratio of two positive reals into this cost. Upstream results include the identity event sitting at the J-cost minimum and structural definitions of defects in related modules that presuppose the same cost structure.
proof idea
This is a one-line wrapper that applies J to the ratio x/y.
why it matters in Recognition Science
This definition supplies the core deviation measure used by all downstream results in the module, including defectDist_nonneg (via J_nonneg), defectDist_symm (via J_reciprocal), and the local quasi-triangle bound with constant K_M. It fills the algebraic role of distance in the Recognition framework, linking directly to J-uniqueness (T5) and enabling the eight-tick octave constructions. It touches the open distinction between local and global triangle inequalities.
scope and limits
- Does not extend to zero or negative reals.
- Does not satisfy the triangle inequality on all positive triples.
- Does not claim to be a metric in the topological sense.
- Does not assign a value independent of the J-cost definition.
Lean usage
theorem defectDist_nonneg (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : 0 ≤ defectDist x y := J_nonneg (x / y) (div_pos hx hy)formal statement (Lean)
310noncomputable def defectDist (x y : ℝ) : ℝ := J (x / y)
proof body
Definition body.
311
312/-- **PROVED: Defect distance is zero at identity.** -/