reciprocal
plain-language theorem explainer
The reciprocal automorphism inverts positive reals while preserving both multiplication and the cost function J. Algebraists classifying symmetries of the cost algebra cite this as the explicit non-identity element of JAut. The definition packages posInv together with direct verification of multiplicativity via commutativity and J-preservation via the reciprocal symmetry theorem.
Claim. The reciprocal automorphism is the map $f(x) = x^{-1}$ on positive reals satisfying $f(xy) = f(x) f(y)$ and $J(f(x)) = J(x)$ for all positive $x, y$.
background
JAut is the type of maps from positive reals to positive reals that are multiplicative under posMul and preserve the cost function J. posInv supplies inversion on positive reals and posMul supplies their multiplication. Upstream J_reciprocal states that J(x) equals J of its reciprocal, which is the invariance used to close the second axiom. This definition lives inside CostAlgebra, the module that equips the positive reals with the algebraic structure required by Recognition Science's cost accounting.
proof idea
The definition supplies posInv as the underlying function and proves the two JAut properties inside a constructor. Multiplicativity is obtained by Subtype.ext followed by simp using posMul, posInv and mul_comm. J-preservation follows immediately from the theorem J_reciprocal applied to the underlying real and its positivity witness.
why it matters
This supplies the non-identity element required by eq_id_or_reciprocal, which classifies every J-automorphism as either the identity or the reciprocal map. It is also invoked inside continuous_bijective_preserves_J_eq_id_or_inv to close the automorphism group under stronger assumptions. In the Recognition framework the construction realizes the inversion symmetry that follows from J-uniqueness, where J(x) = J(1/x) encodes the double-entry balance of costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.