eq_id_or_reciprocal
plain-language theorem explainer
Every J-automorphism on positive reals is either the identity or the reciprocal map. Researchers classifying symmetries under the Recognition Composition Law cite this result to restrict transformations that preserve both multiplication and J-cost. The proof splits on the image of the point 2 under f and reduces each branch to the identity via composition with the reciprocal.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. Every map $f : (0,∞) → (0,∞)$ that satisfies $f(xy) = f(x)f(y)$ and $J(f(x)) = J(x)$ for all $x,y > 0$ equals the identity or the map $x ↦ x^{-1}$.
background
JAut is the subtype of maps on positive reals that preserve multiplication and the value of the J-cost function. The J-cost is defined by J(x) = ½(x + x⁻¹) − 1 and is the unique function satisfying the Recognition Composition Law. Upstream lemmas establish that any element of JAut sends each point to itself or its reciprocal and that any such map fixing the distinguished point 2 must be the identity everywhere.
proof idea
The proof performs rcases on eq_self_or_inv applied to f and posTwo. The left branch invokes eq_id_of_map_two_eq_two directly. The right branch constructs the composition of reciprocal with f, verifies it equals id by evaluation at posTwo, then applies JAut.ext and simplification to obtain equality on all arguments.
why it matters
This supplies the exact algebraic classification of Aut(J) invoked by continuous_bijective_preserves_J_eq_id_or_inv to obtain the paper-facing automorphism theorem. It closes the T5 J-uniqueness step of the forcing chain by showing that the only automorphisms are id and reciprocal, and it is used to define the two-point coding equivFinTwo.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.