J_reciprocal
The theorem asserts that the J-cost function is invariant under taking reciprocals for positive reals. Researchers constructing canonical cost algebras or proving symmetry of defect distances cite this property when building recognition systems from the Recognition Composition Law. The proof is a one-line wrapper that invokes the Jcost_symm lemma directly on the positivity hypothesis.
claimFor every positive real number $x$, $J(x) = J(x^{-1})$, where $J(x) = ½(x + x^{-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$. The CostAlgebra module develops its algebraic properties on the positive reals, including composition, normalization at 1, and defect distances derived from it. The result depends on the Jcost_symm lemma from the Cost module, which establishes the same equality at the level of the underlying Jcost definition before normalization to J.
proof idea
The proof is a one-line wrapper that applies the Jcost_symm lemma to the hypothesis hx : 0 < x.
why it matters in Recognition Science
This symmetry supplies the symmetric field in the canonicalCostAlgebra definition, which packages J together with RCL_holds, J_at_one, and J_nonneg as the standard CostAlgebraData. It is invoked to prove defectDist_symm and J_eq_iff_eq_or_inv, and it appears in mechanical_thermal_symmetric for ultrasound thresholds. In the framework it encodes the double-entry property required by the Recognition Composition Law and supports invariance on the phi-ladder.
scope and limits
- Does not apply when x ≤ 0.
- Does not claim uniqueness of J without the functional equation axioms.
- Does not supply numerical bounds on the cost value.
- Does not extend the symmetry to complex arguments or other fields.
Lean usage
example (x : ℝ) (hx : 0 < x) : J x = J x⁻¹ := J_reciprocal x hxformal statement (Lean)
71theorem J_reciprocal (x : ℝ) (hx : 0 < x) : J x = J x⁻¹ :=
proof body
Term-mode proof.
72 Jcost_symm hx
73
74/-- **Non-negativity**: All costs are non-negative on ℝ₊. -/