defectDist_symm
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove non-negativity of defect distance.
- Does not establish the triangle inequality.
- Applies only to strictly positive real arguments.
- Does not derive the explicit closed form of J.
- Does not connect to physical constants or spatial dimensions.
formal statement (Lean)
319theorem defectDist_symm (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
320 defectDist x y = defectDist y x := by
proof body
Term-mode proof.
321 unfold defectDist
322 have h : x / y > 0 := div_pos hx hy
323 rw [J_reciprocal (x / y) h]
324 congr 1
325 field_simp
326
327/-- **PROVED: Defect distance is non-negative.** -/