defectDist_symm
plain-language theorem explainer
Defect distance d(x,y) defined as J(x/y) for positive reals satisfies d(x,y)=d(y,x). Modelers of cost functionals in Recognition Science cite this to confirm symmetry before metric constructions or composition laws. The term proof unfolds the definition, applies reciprocal invariance of J to the ratio x/y, and finishes with congruence plus field simplification.
Claim. For all real numbers $x>0$ and $y>0$, $J(x/y)=J(y/x)$, where $J$ is the cost function obeying $J(z)=J(z^{-1})$ for $z>0$.
background
In the CostAlgebra module the defect distance is defined by defectDist x y := J (x / y). Its documentation states that this quantity measures the cost of deviation between positive reals and lists the three properties d(x,x)=0, d(x,y)=d(y,x) from J reciprocity, and non-negativity. The supporting J_reciprocal theorem encodes that cost is invariant under inversion, described as the algebraic encoding of double-entry bookkeeping in which every ratio and its reciprocal carry the same cost. The module sits inside the Recognition Science derivation of physics from a single functional equation, importing the core Cost and FunctionalEquation developments.
proof idea
The term proof unfolds defectDist to expose J(x/y). It introduces the auxiliary fact that x/y > 0 by div_pos. Rewriting with the local J_reciprocal lemma on that ratio produces J(x/y) = J((x/y)^{-1}). Congruence followed by field_simp then identifies the inverted ratio with y/x.
why it matters
The result discharges the symmetry claim asserted inside the defectDist documentation, thereby completing the basic algebraic properties required for any later metric interpretation of deviation cost. It supports structures appearing in CPM.LNALBridge and SimplicialLedger.EdgeLengthFromPsi while remaining inside the Recognition Composition Law and the J-uniqueness step of the forcing chain. No open scaffolding questions are closed here, but the symmetry is a prerequisite for treating defect distance as a symmetric cost measure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.