defectDist_self
plain-language theorem explainer
The defect distance between a positive real and itself is zero. Algebraists building cost functions and deviation measures in Recognition Science cite this identity to anchor the zero-cost property of the identity element. The proof reduces the argument of J to unity by cancellation of the ratio and invokes the normalization that J at one equals zero.
Claim. For every positive real number $x > 0$, the defect distance $d(x,x) = 0$, where $d(x,y) := J(x/y)$ and $J$ is the cost function normalized so that $J(1) = 0$.
background
Defect distance is introduced as the map sending a pair of positive reals to the cost of their ratio: $d(x,y) = J(x/y)$. The CostAlgebra module assembles algebraic identities for this map, including the identity, symmetry, and non-negativity properties that follow from the underlying functional equation satisfied by J. The upstream normalization result states that the multiplicative identity carries zero cost, which is the algebraic encoding of the double-entry principle in the Recognition framework.
proof idea
The proof unfolds the definition of defect distance to obtain J of the ratio x/x. It rewrites that ratio to one by invoking the hypothesis that x is positive, then concludes by direct appeal to the theorem establishing J(1) = 0.
why it matters
This result confirms the identity axiom for defect distance, a prerequisite for treating it as a deviation measure inside the cost algebra. It fills the first listed property in the defect-distance documentation and supports later constructions that rely on zero self-cost, such as ledger edge lengths and mechanism-design statements. It sits inside the algebraic layer that precedes the forcing-chain steps T5 through T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.