reciprocalAuto
reciprocalAuto supplies the map sending each real to its multiplicative inverse as the fundamental automorphism of the cost algebra. Algebraists working on J-functional symmetries cite this definition when establishing involution or preservation results. It is realized as a direct one-line abbreviation of the standard reciprocal on the reals.
claimThe reciprocal automorphism is the function $f : ℝ → ℝ$ defined by $f(x) = x^{-1}$.
background
In the CostAlgebra module the algebraic structure is built around the J-cost function obeying the Recognition Composition Law. The reciprocal map supplies the basic symmetry that inverts ratios while leaving this structure intact. Upstream, the sibling reciprocal definition constructs a JAut by verifying preservation of posMul and posInv, while the LedgerForcing reciprocal inverts the ratio of a RecognitionEvent.
proof idea
This declaration is a one-line definition that directly invokes the reciprocal operation on the reals.
why it matters in Recognition Science
The definition supplies the symmetry used to prove that the map is an involution and preserves J-cost in the downstream theorems reciprocal_involution and reciprocal_preserves_cost. It embodies the T5 J-uniqueness step of the forcing chain, where J incorporates the inverse term, and supports the phi-ladder and eight-tick octave constructions.
scope and limits
- Does not restrict inputs to positive reals in the type signature.
- Does not verify involution or cost-preservation properties.
- Does not reference the Recognition Composition Law or phi fixed point.
formal statement (Lean)
688noncomputable def reciprocalAuto : ℝ → ℝ := fun x => x⁻¹
proof body
Definition body.
689
690/-- **PROVED: The reciprocal map is an involution.** -/