reciprocal_preserves_cost
plain-language theorem explainer
reciprocal_preserves_cost shows that J-cost is unchanged when a positive real is replaced by its reciprocal. Algebraists working on the Recognition Composition Law cite it to confirm that inversion is a cost-preserving symmetry of the algebra. The proof is a one-line term that unfolds reciprocalAuto and invokes the symmetry of J_reciprocal.
Claim. Let $J(y) = ½(y + y^{-1}) - 1$. For every $x > 0$, $J(x^{-1}) = J(x)$.
background
The J-cost function is the unique cost satisfying the Recognition Composition Law, given explicitly by $J(x) = ½(x + x^{-1}) - 1$. In the CostAlgebra module this encodes the cost of multiplicative ratios arising from recognition events. reciprocalAuto is the map $x ↦ x^{-1}$, the fundamental inversion symmetry of the algebra. An upstream theorem establishes the invariance $J(x) = J(x^{-1})$ for $x > 0$, which is the algebraic encoding of double-entry bookkeeping for ratios.
proof idea
This is a one-line term-mode wrapper. It unfolds the definition of reciprocalAuto to obtain the inverse, then applies the symmetry lemma J_reciprocal and takes the symmetric form of the resulting equality.
why it matters
The result confirms cost invariance under the reciprocal map, reinforcing the double-entry symmetry already present in J_reciprocal. It supports the uniqueness of J under the Recognition Composition Law and the self-similar fixed-point structure that forces phi. In the forcing chain this property is required before composing costs across recognition events and before deriving the eight-tick octave and three-dimensional geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.