J_reciprocal
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.