reciprocal_involution
The map x to 1/x on the reals is an involution. Algebraists working inside the cost algebra of Recognition Science cite this when confirming that the fundamental inversion symmetry closes after two steps. The proof is a one-line term wrapper that unfolds the definition and invokes the standard involution property of multiplicative inversion.
claimThe map sending each real number $x$ to its multiplicative inverse satisfies $r(r(x)) = x$ for all $x$ in the reals.
background
In the CostAlgebra module the reciprocalAuto function is defined as the map $x mapsto x^{-1}$. This is presented as the fundamental symmetry of the cost algebra. Upstream definitions include the reciprocal automorphism in the same module, the reciprocal event in LedgerForcing that inverts ratios, and the cost functions in ObserverForcing and MultiplicativeRecognizerL4 that derive J-cost from recognition events.
proof idea
The proof is a one-line term-mode wrapper. It unfolds reciprocalAuto to expose ordinary inversion on the reals, then applies the library fact inv_inv that inversion is an involution.
why it matters in Recognition Science
This result confirms that the inversion symmetry of the cost algebra has order two. It supplies a basic algebraic closure property required before the Recognition Composition Law and higher forcing steps (T5 J-uniqueness through T8) can be applied to composed recognition events. No downstream theorems currently reference it, leaving its use in larger derivations open.
scope and limits
- Does not restrict the domain to positive reals.
- Does not prove preservation of J-cost under the map.
- Does not address division by zero or sign changes.
formal statement (Lean)
691theorem reciprocal_involution (x : ℝ) :
692 reciprocalAuto (reciprocalAuto x) = x := by
proof body
Term-mode proof.
693 unfold reciprocalAuto
694 exact inv_inv x
695
696/-- **PROVED: The reciprocal map preserves J-cost.** -/