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