eq_self_or_inv
plain-language theorem explainer
Any J-automorphism of the positive reals maps each point to itself or its reciprocal. Researchers classifying maps that preserve both multiplication and the J-cost in the Recognition framework cite this dichotomy. The argument equates J-values via cost preservation, invokes the level-set classification of J, and recovers the subtype elements.
Claim. Let $f$ be a J-automorphism of the positive reals and let $x>0$. Then $f(x)=x$ or $f(x)=x^{-1}$.
background
The J-cost is the function $J(x)=½(x+x^{-1})-1$ on positive reals, the unique solution to the Recognition Composition Law. PosReal is the subtype of positive reals; posInv denotes the reciprocal map on this subtype. JAut is the type of maps that are multiplicative and satisfy $J(f(x))=J(x)$ for all $x$ (see the definition of JAut).
proof idea
The proof applies the cost-preservation property of any JAut to obtain $J(f x)=J x$. It then calls J_eq_iff_eq_or_inv on the underlying positive reals to split into the equality or reciprocal case. Each branch is lifted by Subtype.ext.
why it matters
This supplies the pointwise case split used by eq_id_of_map_two_eq_two (any automorphism fixing 2 is the identity) and by eq_id_or_reciprocal (every J-automorphism is id or reciprocal). It completes the local analysis needed for the global classification of automorphisms in the cost algebra, which rests on the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.