reciprocal_preserves_cost
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not extend the equality to non-positive reals.
- Does not address preservation under multiplication or other group operations.
- Does not derive the explicit formula for J or prove its uniqueness.
- Does not connect the symmetry to physical constants or dimensional forcing.
formal statement (Lean)
697theorem reciprocal_preserves_cost (x : ℝ) (hx : 0 < x) :
698 J (reciprocalAuto x) = J x := by
proof body
Term-mode proof.
699 unfold reciprocalAuto
700 exact (J_reciprocal x hx).symm
701
702/-- Exact level-set classification for `J` on positive reals:
703 equal cost means equal ratio or reciprocal ratio. -/