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 the automorphism group of the canonical cost algebra cite this when reducing global statements to pointwise choices. The proof is a direct term reduction that applies cost preservation to reach the level-set lemma J_eq_iff_eq_or_inv and lifts via subtype extensionality.
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
J is the cost function $J(x)=½(x+x^{-1})-1$ on positive reals, the unique solution to the Recognition Composition Law. PosReal is the subtype {x:ℝ // 0<x}. JAut consists of multiplicative maps PosReal→PosReal that also preserve J-values. The key upstream lemma J_eq_iff_eq_or_inv states that J y = J x on positive reals if and only if y=x or y=x^{-1}. preserves_cost extracts the J-preservation property from the JAut definition.
proof idea
Apply preserves_cost to obtain J((f x).1)=J(x.1). Feed this into J_eq_iff_eq_or_inv to split into the two cases at the level of underlying reals. In each branch apply Subtype.ext to recover the PosReal equality.
why it matters
This supplies the pointwise disjunction used by eq_id_or_reciprocal to conclude that every J-automorphism is either the identity or the reciprocal map, and by eq_id_of_map_two_eq_two to force the identity when 2 is fixed. It completes the local analysis of symmetries in the cost algebra and supports the J-uniqueness step (T5) in the forcing chain by restricting admissible automorphisms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.